From 1c191c1ec748b22846d516641e014d2b072544e1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Jul 2014 15:02:33 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): instantiate assigned metavariables before collecting unassigned ones Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 1201ea13c..9314f7066 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1120,9 +1120,12 @@ public: } } - expr solve_unassigned_mvars(substitution & subst, expr const & e, name_set & visited) { + expr solve_unassigned_mvars(substitution & subst, expr e, name_set & visited) { + e = subst.instantiate(e); buffer mvars; collect_metavars(e, mvars); + if (mvars.empty()) + return e; for (auto mvar : mvars) { check_interrupted(); solve_unassigned_mvar(subst, mvar, visited);