Stream: Coq devs & plugin devs

Topic: Splitting

view this post on Zulip Hugo Herbelin (Dec 12 2021 at 08:24):

Hi, is rather big (2500 lines). For #12324, I would need to use in the middle of, so that commands browsing notations can work also with "abbreviations"/syntactic-definitions.
More generally, it seems to me that splitting 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 which contains the uninterpretation part of 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 into (wasn't it already suggested actually) and (and all SynDef things) into (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: May 31 2023 at 15:01 UTC