From 034bc2674029e53c282efd2cb220221480565c8c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 8 Jan 2025 13:04:31 +0000 Subject: [PATCH] feat: make `classical` tactic incremental (#6575) This PR ensures tactics are evaluated incrementally in the body of `classical`. --- src/Lean/Elab/Tactic/Classical.lean | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/Lean/Elab/Tactic/Classical.lean b/src/Lean/Elab/Tactic/Classical.lean index 787310edc0..1a1aeacf6c 100644 --- a/src/Lean/Elab/Tactic/Classical.lean +++ b/src/Lean/Elab/Tactic/Classical.lean @@ -24,11 +24,8 @@ def classical [Monad m] [MonadEnv m] [MonadFinally m] [MonadLiftT MetaM m] (t : finally modifyEnv Meta.instanceExtension.popScope -@[builtin_tactic Lean.Parser.Tactic.classical] -def evalClassical : Tactic := fun stx => do - match stx with - | `(tactic| classical $tacs:tacticSeq) => - classical <| Elab.Tactic.evalTactic tacs - | _ => throwUnsupportedSyntax +@[builtin_tactic Lean.Parser.Tactic.classical, builtin_incremental] +def evalClassical : Tactic := fun stx => + classical <| Term.withNarrowedArgTacticReuse (argIdx := 1) Elab.Tactic.evalTactic stx end Lean.Elab.Tactic