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
comNotation.ml (wasn't it already suggested actually) and
syntax_def.ml (and all
SynDef things) into
sounds good to me too
Last updated: Feb 01 2023 at 15:04 UTC