Hi, notation.ml
is rather big (2500 lines). For #12324, I would need to use syntax_def.ml
in the middle of notation.ml
, so that commands browsing notations can work also with "abbreviations"/syntactic-definitions.
More generally, it seems to me that splitting notation.ml
in smaller delimited pieces would make it easier to undertand, maintain and extend. Any opinions?
A first step (for the purpose of #12324) would be to have a notationextern.ml
which contains the uninterpretation
part of notation.ml
. Any objection or suggestion? Cc @Emilio Jesús Gallego Arias.
Since there is a move at organizing the code in a more intelligible way, a parallel suggestion is to rename metasyntax.ml
into comNotation.ml
(wasn't it already suggested actually) and syntax_def.ml
(and all SynDef
things) into abbreviation.ml
(and Abbrev
things).
sounds fine
sounds good to me too
Last updated: May 31 2023 at 15:01 UTC