From 7793efe5c9ac8ff4c71579e6fc0aa4764dd2bc9e Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 1 Jul 2005 14:38:10 +0000
Subject: [PATCH] on is now a keyword (needed in let rec)

---
 helm/ocaml/cic_disambiguation/cicTextualLexer2.ml  | 2 +-
 helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index e67613091..32d8ae54d 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
@@ -66,7 +66,7 @@ let keywords = Hashtbl.create 17
 let _ =
   List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword))
     [ "Prop"; "Type"; "Set"; "let"; "Let"; "rec"; "using"; "match"; "with";
-      "in"; "and"; "to"; "as" ]
+    "in"; "and"; "to"; "as"; "on"]
 
 let error lexbuf msg =
   raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg))
diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index a879ccf94..25c15c575 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -181,7 +181,7 @@ EXTEND
     [ defs = LIST1 [
         name = IDENT;
         args = LIST1 [arg = arg -> arg];
-        index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
+        index_name = OPT [ "on"; idx = IDENT -> idx ];
         ty = OPT [ SYMBOL ":" ; t = term -> t ];
         SYMBOL <:unicode<def>> (* ≝ *);
         t1 = term ->
-- 
2.39.2