From 444a1e5087b872a07ce43dda40211f9e3613d647 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 30 Jan 2004 08:13:56 +0000
Subject: [PATCH] - 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

---
 .../cic_disambiguation/cicTextualParser2.ml   | 48 +++++++++++--------
 1 file changed, 28 insertions(+), 20 deletions(-)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 42b75e9dd..507d897fb 100644
--- 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;
-- 
2.39.2