From 2e5ad274a594e5a53dca6243fa54888dc59032fe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 27 Oct 2014 10:31:09 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): remove invalid assertions

These assertions became invalid when we changed the behavior of undef
indentifiers at

https://github.com/leanprover/lean/commit/8e6de933948748b26ff685bedb76f3e691df9e36
---
 src/frontends/lean/elaborator.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index e6921ac9fe..2dbbfc2c3c 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1111,8 +1111,6 @@ auto elaborator::operator()(list<expr> const & ctx, expr const & e, bool _ensure
 
 std::tuple<expr, expr, level_param_names> elaborator::operator()(
     expr const & t, expr const & v, name const & n, bool is_opaque) {
-    lean_assert(!has_local(t));
-    lean_assert(!has_local(v));
     constraint_seq t_cs;
     expr r_t      = ensure_type(visit(t, t_cs), t_cs);
     // Opaque definitions in the main module may treat other opaque definitions (in the main module) as transparent.