From eef3debcf582d02509b469125cd66d7c259ee7d8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Jun 2016 14:50:01 -0700
Subject: [PATCH] fix(library/type_context): bug in revert with let-decls

---
 src/library/type_context.cpp    |  8 +++++++-
 tests/lean/run/assert_tac1.lean | 17 +++++++++++++++++
 2 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 38165742a6..182d5cd533 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -274,7 +274,13 @@ expr type_context::revert(unsigned num, expr const * locals, expr const & mvar)
                 return static_cast<bool>(m_mctx.get_metavar_decl(mvar)->get_context().get_local_decl(l)); }));
     buffer<expr> reverted;
     expr new_mvar = revert_core(num, locals, mvar, reverted);
-    expr r = mk_app(new_mvar, reverted);
+    expr r = new_mvar;
+    for (expr const & a : reverted) {
+        if (!m_lctx.get_local_decl(a)->get_value()) {
+            // 'a' is not a let-decl
+            r = mk_app(r, a);
+        }
+    }
     m_mctx.assign(mvar, r);
     return r;
 }
diff --git a/tests/lean/run/assert_tac1.lean b/tests/lean/run/assert_tac1.lean
index f53d26d5c2..c7f99b77db 100644
--- a/tests/lean/run/assert_tac1.lean
+++ b/tests/lean/run/assert_tac1.lean
@@ -8,3 +8,20 @@ by do
    exact a,
    x ← get_local "x",
    mk_app ("eq" <.> "refl") [x] >>= exact
+
+print tst1
+
+definition tst2 (a : nat) : a = a :=
+by do
+   assert "x" (expr.const "nat" []),
+   a ← get_local "a",
+   exact a,
+   trace "------------",
+   trace_state,
+   revert "x",
+   intro "y",
+   trace_state,
+   y ← get_local "y",
+   mk_app ("eq" <.> "refl") [y] >>= exact
+
+print tst2