From b7ca2a0ec977d0d0d44046f58b4b32f536979e84 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Apr 2015 17:23:09 -0700
Subject: [PATCH] fix(library/tactic/exact_tactic): exact and or_else

fixes #543
---
 src/library/tactic/exact_tactic.cpp         | 15 ++++++++++++---
 tests/lean/exact_partial.lean.expected.out  | 10 ++++++++++
 tests/lean/exact_partial2.lean              |  4 ++++
 tests/lean/exact_partial2.lean.expected.out | 21 +++++++++++++++++++++
 tests/lean/run/543.lean                     |  4 ++++
 5 files changed, 51 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/exact_partial2.lean
 create mode 100644 tests/lean/exact_partial2.lean.expected.out
 create mode 100644 tests/lean/run/543.lean

diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp
index be9e5a234..f54804e7f 100644
--- a/src/library/tactic/exact_tactic.cpp
+++ b/src/library/tactic/exact_tactic.cpp
@@ -33,9 +33,18 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type
                 return none_proof_state();
             }
             expr t                 = head(gs).get_type();
-            bool report_unassigned = false;
-            if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t),
-                                                       report_unassigned, enforce_type_during_elaboration)) {
+            bool report_unassigned = enforce_type_during_elaboration;
+            optional<expr> new_e;
+            try {
+                new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t),
+                                                  report_unassigned, enforce_type_during_elaboration);
+            } catch (exception &) {
+                if (s.report_failure())
+                    throw;
+                else
+                    return none_proof_state();
+            }
+            if (new_e) {
                 goals const & gs   = new_s.get_goals();
                 if (gs) {
                     goal const & g     = head(gs);
diff --git a/tests/lean/exact_partial.lean.expected.out b/tests/lean/exact_partial.lean.expected.out
index 5c0d29084..ce63e3b2c 100644
--- a/tests/lean/exact_partial.lean.expected.out
+++ b/tests/lean/exact_partial.lean.expected.out
@@ -1,3 +1,13 @@
+exact_partial.lean:4:19: error: don't know how to synthesize placeholder
+a b : Prop,
+a_1 : a,
+a_2 : b
+⊢ a
+exact_partial.lean:4:21: error: don't know how to synthesize placeholder
+a b : Prop,
+a_1 : a,
+a_2 : b
+⊢ b
 exact_partial.lean:4:2: error:invalid 'exact' tactic, term still contains metavariables after elaboration
   and.intro ?M_1 ?M_2
 proof state:
diff --git a/tests/lean/exact_partial2.lean b/tests/lean/exact_partial2.lean
new file mode 100644
index 000000000..022ee2006
--- /dev/null
+++ b/tests/lean/exact_partial2.lean
@@ -0,0 +1,4 @@
+example (a b c : nat) (h₁ : a = b) (h₂ : b = c) : a = c :=
+begin
+  exact (eq.trans h₁ _)
+end
diff --git a/tests/lean/exact_partial2.lean.expected.out b/tests/lean/exact_partial2.lean.expected.out
new file mode 100644
index 000000000..d470edfd8
--- /dev/null
+++ b/tests/lean/exact_partial2.lean.expected.out
@@ -0,0 +1,21 @@
+exact_partial2.lean:3:21: error: don't know how to synthesize placeholder
+a b c : nat,
+h₁ : a = b,
+h₂ : b = c
+⊢ b = c
+exact_partial2.lean:3:2: error:invalid 'exact' tactic, term still contains metavariables after elaboration
+  eq.trans h₁ ?M_1
+proof state:
+a b c : nat,
+h₁ : a = b,
+h₂ : b = c
+⊢ a = c
+exact_partial2.lean:4:0: error: don't know how to synthesize placeholder
+a b c : nat,
+h₁ : a = b,
+h₂ : b = c
+⊢ a = c
+exact_partial2.lean:4:0: error: failed to add declaration '14.0' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a b c : nat) (h₁ : …) (h₂ : …),
+    ?M_1
diff --git a/tests/lean/run/543.lean b/tests/lean/run/543.lean
new file mode 100644
index 000000000..a47caa5e1
--- /dev/null
+++ b/tests/lean/run/543.lean
@@ -0,0 +1,4 @@
+example (a b c : nat) (h₁ : a = b) (h₂ : b = c) : b = c :=
+begin
+  (exact h₁ | exact h₂)
+end