From 9818de078bd60cbfbf6c04448209f892af6a07e7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 May 2022 07:24:23 -0700 Subject: [PATCH] fix: fixes #1168 --- src/Lean/Meta/Tactic/Split.lean | 2 +- tests/lean/run/1168.lean | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/1168.lean diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index ed92ba713f..c6c4b1ec0a 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -137,7 +137,7 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N mkLambdaFVars (ys++altEqsNew) body altsNew := altsNew.push altNew return .done { matcherApp with alts := altsNew }.toExpr - transform e pre + transform (← instantiateMVars e) pre let targetNew ← mkNewTarget (← getMVarType mvarId) unless (← foundRef.get) do throwError "'applyMatchSplitter' failed, did not find discriminants" diff --git a/tests/lean/run/1168.lean b/tests/lean/run/1168.lean new file mode 100644 index 0000000000..0a0be0e0ce --- /dev/null +++ b/tests/lean/run/1168.lean @@ -0,0 +1,3 @@ +theorem ex : True ∧ (match True with | _ => True) := by + constructor; exact trivial + split; trivial