From 8bcaafb28b7d56c4fbb122f5db8fadf88d7827ad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 6 Mar 2022 07:50:19 -0800
Subject: [PATCH] fix: universe metavariables should not be taken into account
 at `getKeyArgs`

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

diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 7cc50c52be..86eb91786b 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -370,7 +370,7 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Ex
   match e.getAppFn with
   | Expr.lit v _       => return (Key.lit v, #[])
   | Expr.const c _ _   =>
-    if (← getConfig).isDefEqStuckEx && e.hasMVar then
+    if (← getConfig).isDefEqStuckEx && e.hasExprMVar then
       if (← isReducible c) then
         /- `e` is a term `c ...` s.t. `c` is reducible and `e` has metavariables, but it was not unfolded.
            This can happen if the metavariables in `e` are "blocking" smart unfolding.