- typo bugfix: INT token no longer exists

- use "=" instead of \def for let definitions
- added a new "binder" level so that \forall n. n=n binds correctly

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 42b75e9dde5b8db6f80caa021bcf5261e81d1d47..507d897fbdea8104181ae767e427e3ed9d3b6957 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -95,14 +95,7 @@ EXTEND
           return_term loc
             (CicTextualParser2Ast.Binder (`Pi, Cic.Anonymous, Some t1, t2))
       ]
-    | "eq" LEFTA
-      [ t1 = term; SYMBOL "="; t2 = term ->
-        return_term loc (CicTextualParser2Ast.Appl_symbol ("eq", 0, [t1; t2]))
-      ]
-    | "add" LEFTA     [ (* nothing here by default *) ]
-    | "mult" LEFTA    [ (* nothing here by default *) ]
-    | "inv" NONA      [ (* nothing here by default *) ]
-    | "simple" NONA
+    | "binder" RIGHTA
       [
         b = binder; vars = LIST1 IDENT SEP SYMBOL ",";
         typ = OPT [ SYMBOL ":"; t = term -> t ];
@@ -119,7 +112,17 @@ EXTEND
               vars body
           in
           return_term loc binder
-      | sort_kind = [
+      ]
+    | "eq" LEFTA
+      [ t1 = term; SYMBOL "="; t2 = term ->
+        return_term loc (CicTextualParser2Ast.Appl_symbol ("eq", 0, [t1; t2]))
+      ]
+    | "add" LEFTA     [ (* nothing here by default *) ]
+    | "mult" LEFTA    [ (* nothing here by default *) ]
+    | "inv" NONA      [ (* nothing here by default *) ]
+    | "simple" NONA
+      [
+        sort_kind = [
           "Prop" -> `Prop | "Set" -> `Set | "Type" -> `Type | "CProp" -> `CProp
         ] ->
           CicTextualParser2Ast.Sort sort_kind
@@ -141,21 +144,26 @@ EXTEND
             return_term loc (CicTextualParser2Ast.Meta (index, substs))
         (* actually "in" and "and" are _not_ keywords. Parsing works anyway
          * since applications are required to be bound by parens *)
-      | "let"; name = IDENT; SYMBOL <:unicode<def>> (* ≝ *); t1 = term;
+      | "let"; name = IDENT;
+(*         SYMBOL <:unicode<def>> (* ≝ *); *)
+        SYMBOL "=";
+        t1 = term;
         IDENT "in"; t2 = term ->
           return_term loc (CicTextualParser2Ast.LetIn (name, t1, t2))
       | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
           defs = LIST1 [
-          name = IDENT;
-          index = OPT [ PAREN "("; index = INT; PAREN ")" ->
-            int_of_string index
-          ];
-          typ = OPT [ SYMBOL ":"; typ = term -> typ ];
-          SYMBOL <:unicode<def>> (* ≝ *); t1 = term ->
-            (name, t1, typ, (match index with None -> 1 | Some i -> i))
-        ] SEP (IDENT "and");
-        IDENT "in"; body = term ->
-          return_term loc (CicTextualParser2Ast.LetRec (ind_kind, defs, body))
+            name = IDENT;
+            index = OPT [ PAREN "("; index = NUM; PAREN ")" ->
+              int_of_string index
+            ];
+            typ = OPT [ SYMBOL ":"; typ = term -> typ ];
+(*             SYMBOL <:unicode<def>> (* ≝ *); *)
+            SYMBOL "=";
+            t1 = term ->
+              (name, t1, typ, (match index with None -> 1 | Some i -> i))
+          ] SEP (IDENT "and");
+          IDENT "in"; body = term ->
+            return_term loc (CicTextualParser2Ast.LetRec (ind_kind, defs, body))
       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
         "match"; t = term;
         SYMBOL ":"; indty = IDENT;