From 3bd83b8e41135a10e2fb4af6cf7801ee67250f64 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 18 Nov 2015 19:14:37 -0800
Subject: [PATCH] feat(library/blast/backward/backward_strategy): don't try
 constructor action by default

---
 src/library/blast/backward/backward_strategy.cpp | 1 -
 tests/lean/run/blast20.lean                      | 2 ++
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/library/blast/backward/backward_strategy.cpp b/src/library/blast/backward/backward_strategy.cpp
index bbd5293f8..75d4d7d3f 100644
--- a/src/library/blast/backward/backward_strategy.cpp
+++ b/src/library/blast/backward/backward_strategy.cpp
@@ -71,7 +71,6 @@ class backward_strategy : public strategy {
         Try(assumption_action());
         list<gexpr> backward_rules = get_extension().get_backward_rule_set().find(head_index(curr_state().get_target()));
         Try(backward_action(backward_rules, true));
-        Try(constructor_action());
         return action_result::failed();
     }
 };
diff --git a/tests/lean/run/blast20.lean b/tests/lean/run/blast20.lean
index aad048516..70ba0de36 100644
--- a/tests/lean/run/blast20.lean
+++ b/tests/lean/run/blast20.lean
@@ -12,6 +12,8 @@ by blast
 example : ∀ (F F' : Prop), F ∧ F' → F :=
 by blast
 
+attribute and.intro [backward]
+
 example : ∀ (P Q R : nat → Prop) (F : Prop), (F ∧ (∀ n m, (Q m ∧ R n) → P n)) →
             (F → R 2) → Q 1 → P 2 ∧ F :=
 by blast