|
|
identifiers (#2158)
. is not an operator in Coq: in this specific usage, it is only meant to build a qualified name, so this rule really corresponds to a proper lexical rule in Coq
Unlike most languages, Coq has a large set of special words that are not reserved: they may still be used as identifiers. For example Prop is a special word, which currently gets highlighted as such in Equations.Prop.Equations, but it should be recognized as a regular name there. Because of how flexible the syntax of Coq is, it's not straightforward to disambiguate things with just a bunch of regexes, so we have to rely on heuristics. Skipping qualified names from being recognized as keywords is an easy win.
|
