From ffc168d63a903e83d8d5e062e8e0ca9bf1df301b Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Sat, 31 Oct 2015 16:53:04 -0700
Subject: [PATCH] fix(frontends/lean/elaborator): visit_app partial

---
 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 4c0b988fbf..9eb05f5faf 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -684,7 +684,7 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) {
                binding_info(f_type).is_inst_implicit()) {
             lean_assert(binding_info(f_type).is_strict_implicit() || !first);
             expr const & d_type = binding_domain(f_type);
-            if (partial_expl || is_pi(whnf(d_type).first))
+            if (partial_expl && is_pi(whnf(d_type).first))
                 break;
             tag g          = f.get_tag();
             bool is_strict = true;