From d0499ebf4d9294d8db5b6ab7bc4e6cc91171ab76 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Jun 2022 10:18:05 -0700 Subject: [PATCH] fix: fixes #1200 --- src/Lean/Meta/Tactic/Split.lean | 2 +- tests/lean/run/1200.lean | 6 ++++++ 2 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/1200.lean diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index 81c2241816..095fd09ca5 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -215,7 +215,7 @@ def applyMatchSplitter (mvarId : MVarId) (matcherDeclName : Name) (us : Array Le trace[Meta.Tactic.split] "after introN\n{mvarId}" let discrsNew := discrFVarIdsNew.map mkFVar let mvarType ← getMVarType mvarId - let elimUniv ← getLevel mvarType + let elimUniv ← withMVarContext mvarId <| getLevel mvarType let us ← if let some uElimPos := info.uElimPos? then pure <| us.set! uElimPos elimUniv diff --git a/tests/lean/run/1200.lean b/tests/lean/run/1200.lean new file mode 100644 index 0000000000..ab113ce2bd --- /dev/null +++ b/tests/lean/run/1200.lean @@ -0,0 +1,6 @@ +example +(h: match .none (α:=α) with +| some _ => True +| _ => True): + True := by + split at h <;> trivial