diff --git a/src/library/blast/strategies/simple_strategy.cpp b/src/library/blast/strategies/simple_strategy.cpp index b3f100405..125c8bd37 100644 --- a/src/library/blast/strategies/simple_strategy.cpp +++ b/src/library/blast/strategies/simple_strategy.cpp @@ -52,8 +52,8 @@ class simple_strategy_fn : public strategy_fn { Try(trivial_action()); Try(assumption_action()); Try(recursor_action()); - Try(constructor_action()); Try(ematch_action()); + Try(constructor_action()); Try(by_contradiction_action()); TryStrategy(mk_backward_strategy()); Try(qfc_action(list())); diff --git a/tests/lean/run/blast_meta_bug.lean b/tests/lean/run/blast_meta_bug.lean new file mode 100644 index 000000000..bb5dc61ff --- /dev/null +++ b/tests/lean/run/blast_meta_bug.lean @@ -0,0 +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 + +example (a : A) : P a → Exists Q := +by blast