56f463e893
. 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.
136 lines
2.8 KiB
Text
Generated
136 lines
2.8 KiB
Text
Generated
'From' Keyword.Namespace
|
|
' ' Text
|
|
'Coq' Name
|
|
' ' Text
|
|
'Require' Keyword.Namespace
|
|
' ' Text
|
|
'Import' Keyword.Namespace
|
|
' ' Text
|
|
'Arith' Name
|
|
'.' Operator
|
|
'\n' Text
|
|
|
|
'Require' Keyword.Namespace
|
|
' ' Text
|
|
'Import' Keyword.Namespace
|
|
' ' Text
|
|
'Equations.Prop.Equations' Name
|
|
'.' Operator
|
|
'\n' Text
|
|
|
|
'Set' Keyword.Namespace
|
|
' ' Text
|
|
'Implicit' Keyword.Namespace
|
|
' ' Text
|
|
'Arguments' Keyword.Namespace
|
|
'.' Operator
|
|
'\n' Text
|
|
|
|
'Set' Keyword.Namespace
|
|
' ' Text
|
|
'Primitive' Name
|
|
' ' Text
|
|
'Projections' Keyword.Namespace
|
|
'.' Operator
|
|
'\n' Text
|
|
|
|
'Unset' Keyword.Namespace
|
|
' ' Text
|
|
'Printing' Keyword.Namespace
|
|
' ' Text
|
|
'All' Keyword.Namespace
|
|
'.' Operator
|
|
'\n' Text
|
|
|
|
'Scheme' Keyword.Namespace
|
|
' ' Text
|
|
'tree_forest_rec' Name
|
|
' ' Text
|
|
':=' Operator
|
|
' ' Text
|
|
'Induction' Name
|
|
' ' Text
|
|
'for' Keyword
|
|
' ' Text
|
|
'tree' Name
|
|
' ' Text
|
|
'Sort' Name
|
|
' ' Text
|
|
'Set' Keyword.Type
|
|
'\n ' Text
|
|
'with' Keyword
|
|
' ' Text
|
|
'forest_tree_rec' Name
|
|
' ' Text
|
|
':=' Operator
|
|
' ' Text
|
|
'Induction' Name
|
|
' ' Text
|
|
'for' Keyword
|
|
' ' Text
|
|
'forest' Name
|
|
' ' Text
|
|
'Sort' Name
|
|
' ' Text
|
|
'Set' Keyword.Type
|
|
'.' Operator
|
|
'\n' Text
|
|
|
|
'Fail' Keyword.Namespace
|
|
' ' Text
|
|
'Definition' Keyword.Namespace
|
|
' ' Text
|
|
'x' Name
|
|
' ' Text
|
|
':' Operator
|
|
' ' Text
|
|
'unit' Name
|
|
' ' Text
|
|
':=' Operator
|
|
' ' Text
|
|
'3' Literal.Number.Integer
|
|
'.' Operator
|
|
'\n' Text
|
|
|
|
'admit' Keyword.Pseudo
|
|
'.' Operator
|
|
'\n' Text
|
|
|
|
'Equations?' Keyword.Namespace
|
|
' ' Text
|
|
'neg' Name
|
|
' ' Text
|
|
'(' Operator
|
|
'b' Name
|
|
' ' Text
|
|
':' Operator
|
|
' ' Text
|
|
'bool' Name
|
|
')' Operator
|
|
' ' Text
|
|
':' Operator
|
|
' ' Text
|
|
'bool' Name
|
|
' ' Text
|
|
':=' Operator
|
|
'\n' Text
|
|
|
|
'neg' Name
|
|
' ' Text
|
|
'true' Name.Builtin.Pseudo
|
|
' ' Text
|
|
':=' Operator
|
|
' ' Text
|
|
'false' Name.Builtin.Pseudo
|
|
';' Operator
|
|
'\n' Text
|
|
|
|
'neg' Name
|
|
' ' Text
|
|
'false' Name.Builtin.Pseudo
|
|
' ' Text
|
|
':=' Operator
|
|
' ' Text
|
|
'true' Name.Builtin.Pseudo
|
|
'.' Operator
|
|
'\n' Text
|