max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: remove unused trace.Elab.syntax option (#3844)

Browse source
This commit is contained in:
Joachim Breitner 2024-04-08 19:16:24 +02:00 • committed by GitHub
parent a82f0d9413
commit 892bfe2c5f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Elab/Syntax.lean
View file

@ -442,7 +442,4 @@ def strLitToPattern (stx: Syntax) : MacroM Syntax :=
| some str => return mkAtomFrom stx str
| none => Macro.throwUnsupported
builtin_initialize
registerTraceClass `Elab.syntax
end Lean.Elab.Command