Hugo Herbelin (Dec 12 2021 at 08:24): Hugo Herbelin (Dec 12 2021 at 08:24):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.
Hugo Herbelin (Dec 12 2021 at 08:28):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).
Gaëtan Gilbert (Dec 12 2021 at 09:29):sounds fine
Emilio Jesús Gallego Arias (Dec 13 2021 at 13:41):sounds good to me too
Last updated: May 31 2023 at 15:01 UTC