]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/cicTextualParser2.ml
on is now a keyword (needed in let rec)
[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml
index a879ccf94ff1f380d011e71927250df3e3c46f3d..25c15c575f9c763e33962106b2912456ed3554d1 100644 (file)
@@ -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 ->