fix(library/tactic/exact_tactic): exact and or_else

fixes #543

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;
+            bool report_unassigned = enforce_type_during_elaboration;
-            if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t),
+            optional<expr> new_e;
-                                                       report_unassigned, enforce_type_during_elaboration)) {
+            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);

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:

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

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

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