Commit 2022-11-15 08:49 cf221b55

View on Github →

chore: remove obsolete CommandQuote (#602)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Deleted Mathlib/Tactic/CommandQuote.lean

deleted def Lean.Elab.Term.elabCommandQuot

deleted def command.quot

Modified scripts/style-exceptions.txt