From af7ffcf5756f8b22867bdd1714a452464a4a2e7b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Dec 2015 12:23:01 -0800
Subject: [PATCH] chore(tests/lean/run/blast_meta_bug): use "ematch" strategy
 in the test

---
 tests/lean/run/blast_meta_bug.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/lean/run/blast_meta_bug.lean b/tests/lean/run/blast_meta_bug.lean
index bb5dc61ff..ca6e04f1b 100644
--- a/tests/lean/run/blast_meta_bug.lean
+++ b/tests/lean/run/blast_meta_bug.lean
@@ -1,7 +1,7 @@
 constants {A : Type.{1}} (P : A → Prop) (Q : A → Prop)
 definition H : ∀ a, (: P a :) → Exists Q := sorry
 
-set_option blast.ematch true
+set_option blast.strategy "ematch"
 
 example (a : A) : P a → Exists Q :=
 by blast