From 3747ba095af5b69b7ee0ffd0f8ea0d3e12b323db Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 20 Aug 2015 17:55:33 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): incorrect assertion

It is supposed to be "!first implies is_local(from)"

fixes #807
---
 src/frontends/lean/elaborator.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 73229c5d9..5b73bb311 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1483,7 +1483,7 @@ expr elaborator::process_obtain_expr(list<obtain_struct> const & s_list, list<ex
         expr r = process_obtain_expr(tail(s_list), tail(from_list), new_goal, false, cs, src);
         return Fun(new_from, r);
     } else {
-        lean_assert(!first || is_local(from));
+        lean_assert(first || is_local(from));
         expr from_type  = whnf(infer_type(from, cs), cs);
         buffer<expr> I_args;
         expr I          = get_app_args(from_type, I_args);