From 496c84dac65bf709b7c5a9677fb546f9911c29b5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 4 Feb 2016 15:14:30 -0800
Subject: [PATCH] fix(frontends/lean/elaborator): fixes #982

---
 src/frontends/lean/elaborator.cpp |  2 +-
 tests/lean/run/982.lean           | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/982.lean

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index e002da543..d596a399c 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2395,7 +2395,7 @@ static expr translate_local_name(environment const & env,
 */
 static expr translate(environment const & env, list<expr> const & ctx, expr const & e) {
     auto fn = [&](expr const & e) {
-        if (is_placeholder(e) || is_by(e)) {
+        if (is_placeholder(e) || is_by(e) || is_by_plus(e)) {
             return some_expr(e); // ignore placeholders
         } else if (is_constant(e)) {
             expr new_e = copy_tag(e, translate_local_name(env, ctx, const_name(e), e));
diff --git a/tests/lean/run/982.lean b/tests/lean/run/982.lean
new file mode 100644
index 000000000..1f1271ecf
--- /dev/null
+++ b/tests/lean/run/982.lean
@@ -0,0 +1,18 @@
+import data.nat
+open nat
+
+constant P : nat → Prop
+
+example (Hex : ∃ n, P n) : true :=
+  obtain n Hn, from Hex,
+  begin+
+    note Hn2 := Hn,
+    exact trivial
+  end
+
+example (Hex : ∃ n, P n) : true :=
+  obtain n Hn, from Hex,
+  begin+
+    have H : n ≥ 0, from sorry,
+    exact trivial
+  end