From 24b35eefe6a365ece5ca749dde62f2045ec377c2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 25 May 2015 14:04:27 -0700
Subject: [PATCH] chore(frontends/lean/elaborator): add assertion for sanity
 checking

---
 src/frontends/lean/elaborator.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index c277ecebf..2d1799758 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1846,6 +1846,7 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
         return false;
     } else {
         subst = ps.get_subst();
+        lean_assert(subst.is_assigned(mvar));
         expr v = subst.instantiate(mvar);
         subst.assign(mlocal_name(mvar), v);
         return true;