From 7f12401ea7ee7310472a3807bb3ebb5a7033c49f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 May 2015 10:16:12 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): save type information for
 'obtain' declarations

---
 src/frontends/lean/elaborator.cpp             |  5 ++-
 tests/lean/interactive/obtain_type_info.input | 16 ++++++++++
 .../obtain_type_info.input.expected.out       | 31 +++++++++++++++++++
 3 files changed, 51 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/interactive/obtain_type_info.input
 create mode 100644 tests/lean/interactive/obtain_type_info.input.expected.out

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index e8818f4918..e41092f694 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1403,7 +1403,10 @@ expr elaborator::process_obtain_expr(list<obtain_struct> const & s_list, list<ex
         lean_assert(is_local(from));
         expr const & from_type = mlocal_type(from);
         // fix user visible name
-        expr goal_domain = visit(binding_domain(goal), cs);
+        expr d0          = binding_domain(goal);
+        expr goal_domain = visit(d0, cs);
+        if (is_placeholder(d0) && !is_explicit_placeholder(d0))
+            save_binder_type(d0, goal_domain);
         expr new_from    = ::lean::mk_local(mlocal_name(from), binding_name(goal), goal_domain, binder_info());
         if (!is_lambda(goal))
             throw_elaborator_exception("invalid 'obtain' expression, insufficient number of local declarations", src);
diff --git a/tests/lean/interactive/obtain_type_info.input b/tests/lean/interactive/obtain_type_info.input
new file mode 100644
index 0000000000..4781d198f4
--- /dev/null
+++ b/tests/lean/interactive/obtain_type_info.input
@@ -0,0 +1,16 @@
+VISIT obtain_type_info.lean
+SYNC 12
+open eq
+inductive I (F : Type₁ → Prop) : Type₁ :=
+mk : I F
+axiom InjI : ∀ {x y}, I x = I y → x = y
+definition P (x : Type₁) : Prop := ∃ a, I a = x ∧ (a x → false).
+definition p := I P
+lemma false_of_Pp (H : P p) : false :=
+obtain a Ha0 Ha1, from H,
+  subst (InjI Ha0) Ha1 H
+lemma contradiction : false :=
+have Pp : P p, from exists.intro P (and.intro rfl false_of_Pp),
+false_of_Pp Pp
+WAIT
+INFO 8
diff --git a/tests/lean/interactive/obtain_type_info.input.expected.out b/tests/lean/interactive/obtain_type_info.input.expected.out
new file mode 100644
index 0000000000..7993a05077
--- /dev/null
+++ b/tests/lean/interactive/obtain_type_info.input.expected.out
@@ -0,0 +1,31 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- SYMBOL|8|0
+obtain
+-- ACK
+-- TYPE|8|7
+Type₁ → Prop
+-- ACK
+-- IDENTIFIER|8|7
+a
+-- ACK
+-- TYPE|8|9
+I a = p
+-- ACK
+-- IDENTIFIER|8|9
+Ha0
+-- ACK
+-- TYPE|8|13
+a p → false
+-- ACK
+-- IDENTIFIER|8|13
+Ha1
+-- ACK
+-- TYPE|8|23
+P p
+-- ACK
+-- IDENTIFIER|8|23
+H
+-- ACK
+-- ENDINFO