Stream: Coq devs & plugin devs

Topic: Splitting notation.ml


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Gaëtan Gilbert (Dec 12 2021 at 09:29):

sounds fine

view this post on Zulip Emilio Jesús Gallego Arias (Dec 13 2021 at 13:41):

sounds good to me too


Last updated: Feb 01 2023 at 15:04 UTC