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?

(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)

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`

So what's the difference between `where_decl_notation`

(in `Metasyntax`

) and `decl_notation`

?

(I mean the difference in terms of intent, I can read the concrete differences)

Also the information carried by `decl_notation`

does not seem more restrictive than the one for a general notation

Anyway, thanks.

Maxime Dénès has marked this topic as resolved.

Last updated: Jun 09 2023 at 08:01 UTC