diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 5b0a7c2b07..255ca0263d 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -218,6 +218,7 @@ builtin_initialize registerParserAlias! "letRecDecls" Term.letRecDecls registerParserAlias! "hole" Term.hole registerParserAlias! "syntheticHole" Term.syntheticHole + registerParserAlias! "matchDiscr" Term.matchDiscr end Parser end Lean