Fixing the "parsing rules with idents later declared as keywords" problem.

The fix was actually elementary. The lexer comes with a function to
compare parsed tokens against tokens of the parsing rules. It is
enough to have this function considering an ident in a parsing rule to
be equal to the corresponding string parsed as a keyword.

2 files changed, 7 insertions, 0 deletions

diff --git a/parsing/tok.ml b/parsing/tok.ml
index efd57968d2..12140f4036 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -21,6 +21,7 @@ type t =
   | EOI
 
 let equal t1 t2 = match t1, t2 with
+| IDENT s1, KEYWORD s2 -> CString.equal s1 s2
 | KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2
 | METAIDENT s1, METAIDENT s2 -> CString.equal s1 s2
 | PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 2371d32cda..b72a067407 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -101,3 +101,9 @@ Fail Check fun x => match x with S (FORALL x, _) => 0 end.
 
 Parameter traverse : (nat -> unit) -> (nat -> unit).
 Notation traverse_var f l := (traverse (fun l => f l) l).
+
+(* Check that when an ident become a keyword, it does not break
+   previous rules relying on the string to be classified as an ident *)
+
+Notation "'intros' x" := (S x) (at level 0).
+Goal True -> True. intros H. exact H. Qed.