From 4fdf74500d6c0069e9ecb92bf809100a2da1ee84 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Thu, 24 Jul 2025 08:57:00 +0200 Subject: [PATCH] fix: Remove duplicate syntax definitions for `mvcgen*` (#9505) This PR removes vestigial syntax definitions in `Lean.Elab.Tactic.Do.VCGen` that when imported undefine the `mvcgen` tactic. Now it should be possible to import Mathlib and still use `mvcgen`. --- src/Lean/Elab/Tactic/Do/VCGen.lean | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/Lean/Elab/Tactic/Do/VCGen.lean b/src/Lean/Elab/Tactic/Do/VCGen.lean index 1ab17cc1a5..65d7051028 100644 --- a/src/Lean/Elab/Tactic/Do/VCGen.lean +++ b/src/Lean/Elab/Tactic/Do/VCGen.lean @@ -96,15 +96,6 @@ def liftSimpM (x : SimpM α) : VCGenM α := do instance : MonadLift SimpM VCGenM where monadLift x := liftSimpM x -syntax (name := mvcgen_step) "mvcgen_step" optConfig - (num)? (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic - -syntax (name := mvcgen_no_trivial) "mvcgen_no_trivial" optConfig - (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic - -syntax (name := mvcgen) "mvcgen" optConfig - (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? : tactic - private def mkSpecContext (optConfig : Syntax) (lemmas : Syntax) (ignoreStarArg := false) : TacticM Context := do let config ← elabConfig optConfig let mut specThms ← getSpecTheorems