From 64788320f2caf238e58b6d74c26ab7e7706da3ac Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 31 Aug 2013 14:24:07 -0700
Subject: [PATCH] Fix elaborator for let-expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 examples/ex15.lean         | 13 ++++++++++++-
 src/library/elaborator.cpp |  6 ++++--
 2 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/examples/ex15.lean b/examples/ex15.lean
index ad1756535..e13f1eab9 100644
--- a/examples/ex15.lean
+++ b/examples/ex15.lean
@@ -1,4 +1,3 @@
-
 Variable N : Type
 Variable h : N -> N -> N
 
@@ -45,3 +44,15 @@ Theorem Example3 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧
 
 Set lean::pp::implicit false
 Show Environment 1
+
+Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) :=
+    DisjCases H
+              (fun H1 : _,
+                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))
+                   in CongrH AeqC (Symm AeqC))
+              (fun H1 : _,
+                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1)
+                   in CongrH AeqC (Symm AeqC))
+
+Set lean::pp::implicit false
+Show Environment 1
diff --git a/src/library/elaborator.cpp b/src/library/elaborator.cpp
index c7128ea6b..e9c219a67 100644
--- a/src/library/elaborator.cpp
+++ b/src/library/elaborator.cpp
@@ -211,7 +211,7 @@ class elaborator::imp {
         }
         case expr_kind::Let: {
             expr lt = infer(let_value(e), ctx);
-            return infer(let_body(e), extend(ctx, let_name(e), lt, let_value(e)));
+            return lower_free_vars_mmv(infer(let_body(e), extend(ctx, let_name(e), lt, let_value(e))), 1, 1);
         }}
         lean_unreachable();
         return expr();
@@ -462,7 +462,8 @@ class elaborator::imp {
                                                                    m_metavars[midx].m_mvar, m_metavars[midx].m_ctx, static_cast<unsigned>(-1)));
                                 progress = true;
                             } catch (exception&) {
-                                // std::cout << "Failed to infer: " << m_metavars[midx].m_assignment << "\nAT\n" << m_metavars[midx].m_ctx << "\n";
+                                // std::cout << "Failed to infer type of: ?M" << midx << "\n"
+                                //          << m_metavars[midx].m_assignment << "\nAT\n" << m_metavars[midx].m_ctx << "\n";
                                 throw unification_type_mismatch_exception(*m_owner, m_metavars[midx].m_ctx, m_metavars[midx].m_mvar);
                             }
                         }
@@ -524,6 +525,7 @@ public:
     }
 
     expr operator()(expr const & e, elaborator const & elb) {
+        // std::cout << "ELABORATIMG: " << e << "\n";
         m_owner = &elb;
         unsigned num_meta = m_metavars.size();
         m_add_constraints = true;