From 21353d07d55791328d08add6cafcb2cde1109430 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Mar 2020 17:31:07 -0700
Subject: [PATCH] fix: unassigned universe metavariables should not block
 instantiation of delayed assignment

---
 src/Init/Lean/MetavarContext.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean
index 29fa7222d3..e4005dbcb4 100644
--- a/src/Init/Lean/MetavarContext.lean
+++ b/src/Init/Lean/MetavarContext.lean
@@ -532,7 +532,7 @@ partial def main : Expr → M Expr
         instArgs f
       else do
         newVal ← visit main val;
-        if newVal.hasMVar then
+        if newVal.hasExprMVar then
           instArgs f
         else do
           args ← args.mapM (visit main);