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.
12 lines
366 B
Text
12 lines
366 B
Text
From Coq Require Import Arith.
|
|
Require Import Equations.Prop.Equations.
|
|
Set Implicit Arguments.
|
|
Set Primitive Projections.
|
|
Unset Printing All.
|
|
Scheme tree_forest_rec := Induction for tree Sort Set
|
|
with forest_tree_rec := Induction for forest Sort Set.
|
|
Fail Definition x : unit := 3.
|
|
admit.
|
|
Equations? neg (b : bool) : bool :=
|
|
neg true := false;
|
|
neg false := true.
|