From 0742b65183fba474d5aeb346e6ec88e27125909a Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Wed, 6 Jul 2016 11:04:03 -0700
Subject: [PATCH] fix(library/metavar_context): comment out problematic
 assertion

---
 src/library/metavar_context.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/library/metavar_context.cpp b/src/library/metavar_context.cpp
index 8fd38eabfa..ae27f4f7a5 100644
--- a/src/library/metavar_context.cpp
+++ b/src/library/metavar_context.cpp
@@ -61,7 +61,11 @@ void metavar_context::assign_core(expr const & e, expr const & v) {
 }
 
 void metavar_context::assign(expr const & e, expr const & v) {
-    lean_assert(!is_assigned(e));
+    // TODO(leo, dhs): confirm that we do not need this assertion
+    // Note: it triggers an assertion failure from
+    // https://github.com/leanprover/lean/blob/lean3/src/library/metavar_util.h#L127-L135
+    // when CTX is a type_context.
+    // lean_assert(!is_assigned(e));
     assign_core(e, v);
 }