Maxime Dénès (Dec 05 2022 at 12:34): Maxime Dénès (Dec 05 2022 at 12:34):Hi! I'm a bit confused by the terminology: shouldn't this be notation_decl? https://github.com/coq/coq/blob/master/vernac/vernacexpr.ml#L165
Or is it really meant to be a "declaration notation" datatype? What would it mean?
Maxime Dénès (Dec 05 2022 at 12:34):(I'm trying to improve the Metasyntax API with the phase separation, so I really need to get this right because the ADT appears naturally in the interface)
Gaëtan Gilbert (Dec 05 2022 at 12:40):it seems to mean "notation attached to a declaration" judging by the usage (the stuff that goes in where for Fixpoint, Inductive, Record)
also in ppvernac pr_decl_notation unconditionally prints with where
Maxime Dénès (Dec 05 2022 at 12:41):So what's the difference between where_decl_notation (in Metasyntax) and decl_notation?
Maxime Dénès (Dec 05 2022 at 12:42):(I mean the difference in terms of intent, I can read the concrete differences)
Maxime Dénès (Dec 05 2022 at 12:43):Also the information carried by decl_notation does not seem more restrictive than the one for a general notation
Maxime Dénès (Dec 05 2022 at 12:53):Anyway, thanks.
Notification Bot (Dec 05 2022 at 12:54):Maxime Dénès has marked this topic as resolved.
Last updated: Jun 09 2023 at 08:01 UTC