From 32eabf2ef10fff6c79691357a67c2fe7f0a118d9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 11 Sep 2020 10:21:57 -0700 Subject: [PATCH] chore: remove old elaborator that is not needed anymore --- src/Lean/Elab/App.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 5728aa28ae..bcb3f70ff1 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -662,9 +662,6 @@ fun stx expectedType? => match_syntax stx with @[builtinTermElab choice] def elabChoice : TermElab := elabAtom @[builtinTermElab proj] def elabProj : TermElab := elabAtom @[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabAtom -/- A raw identiier is not a valid term, - but it is nice to have a handler for them because it allows `macros` to insert them into terms. -/ -@[builtinTermElab ident] def elabRawIdent : TermElab := elabAtom @[init] private def regTraceClasses : IO Unit := do registerTraceClass `Elab.app;