From 408005b730c0ec7afe8f09ff10cdf6139cc1052b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Sep 2013 09:56:33 -0700 Subject: [PATCH] Fix typo Signed-off-by: Leonardo de Moura --- src/frontends/lean/lean_elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/lean_elaborator.cpp b/src/frontends/lean/lean_elaborator.cpp index cf4243f16e..5155109bc6 100644 --- a/src/frontends/lean/lean_elaborator.cpp +++ b/src/frontends/lean/lean_elaborator.cpp @@ -543,8 +543,8 @@ class elaborator::imp { } } } else if (is_type(lhs) && is_type(rhs)) { + // ignoring type universe levels. We let the kernel check that delayed = 0; - return; // ignoring type universe levels. We let the kernel check that } else if (is_abstraction(lhs) && is_abstraction(rhs)) { delayed = 0; m_constraints.push_back(constraint(abst_domain(lhs), abst_domain(rhs), c));