From 5d38a5a5cdcdbdd8a9e3e5df98c04dacac6ef789 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 4 Dec 2015 14:03:51 -0800
Subject: [PATCH] test(tests/lean/run/blast_ematch10): make sure the test is
 for the `cc` module

---
 tests/lean/run/blast_ematch10.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/tests/lean/run/blast_ematch10.lean b/tests/lean/run/blast_ematch10.lean
index 65c213b65..61890f120 100644
--- a/tests/lean/run/blast_ematch10.lean
+++ b/tests/lean/run/blast_ematch10.lean
@@ -1,4 +1,9 @@
 attribute iff [reducible]
+set_option blast.subst false
+set_option blast.simp  false
 
-example (p : nat → Prop) (a b c : nat) : p a → a = b → p b :=
+definition lemma1 (p : nat → Prop) (a b c : nat) : p a → a = b → p b :=
 by blast
+
+set_option pp.beta true
+print lemma1