From e0209a1532a9a25617ad361b74845cf1f34978eb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Jul 2015 18:07:57 -0700
Subject: [PATCH] feat(frontends/lean): better error localization for
 'have'-expressions in tactic mode

---
 src/frontends/lean/builtin_exprs.cpp     |  2 +-
 tests/lean/have_tactic.lean              |  5 +++++
 tests/lean/have_tactic.lean.expected.out | 18 ++++++++++++++++++
 3 files changed, 24 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/have_tactic.lean
 create mode 100644 tests/lean/have_tactic.lean.expected.out

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 65d20c6bd..2e682dd5f 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -222,7 +222,7 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
                         p.next();
                         auto pos = p.pos();
                         expr t = p.parse_tactic_expr_arg();
-                        t      = p.mk_app(get_rexact_tac_fn(), t, pos);
+                        t      = p.mk_app(get_exact_tac_fn(), t, pos);
                         t      = p.save_pos(mk_begin_end_element_annotation(t), pos);
                         t      = p.save_pos(mk_begin_end_annotation(t), pos);
                         add_tac(t, pos);
diff --git a/tests/lean/have_tactic.lean b/tests/lean/have_tactic.lean
new file mode 100644
index 000000000..309c5239a
--- /dev/null
+++ b/tests/lean/have_tactic.lean
@@ -0,0 +1,5 @@
+example (a b c : nat) : a = b → b = c → a = c :=
+begin
+  intro h₁ h₂,
+  have a = c, from eq.trans h₁ _,
+end
diff --git a/tests/lean/have_tactic.lean.expected.out b/tests/lean/have_tactic.lean.expected.out
new file mode 100644
index 000000000..d152d5ac2
--- /dev/null
+++ b/tests/lean/have_tactic.lean.expected.out
@@ -0,0 +1,18 @@
+have_tactic.lean:4:31: error: don't know how to synthesize placeholder
+a b c : nat,
+h₁ : a = b,
+h₂ : b = c
+⊢ b = c
+have_tactic.lean:4:19: 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
+have_tactic.lean:5:0: error: don't know how to synthesize placeholder
+a b c : nat
+⊢ a = b → b = c → a = c
+have_tactic.lean:5:0: error: failed to add declaration 'example' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  ?M_1