From 556861c8d6aa4852d49d7ec37d508ccdee315d77 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 26 Jul 2014 07:52:10 -0700
Subject: [PATCH] fix(library/unifier): remove incorrect assertion

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/unifier.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 38fc68c56..b5bb77c19 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -1199,7 +1199,6 @@ struct unifier_fn {
     */
     void mk_simple_nonlocal_projection(expr const & m, buffer<expr> const & margs, unsigned i, expr const & rhs, justification const & j,
                               buffer<constraints> & alts) {
-        lean_assert(!is_local(rhs));
         expr const & mtype = mlocal_type(m);
         unsigned vidx = margs.size() - i - 1;
         expr const & marg = margs[i];