From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 10 Jun 2005 16:02:39 +0000 (+0000)
Subject: The type of the left parameters of an inductive type can now be omitted.
X-Git-Tag: PRE_STORAGE~72
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e68d48a7da1d3bf28442e6fa9206e26bd765e187;p=helm.git

The type of the left parameters of an inductive type can now be omitted.
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 4b94226cb..951028745 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -171,15 +171,16 @@ EXTEND
         (head, vars)
     ]
   ];
+  arg: [
+   [ PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
+      SYMBOL ":"; ty = term; PAREN ")" -> names,ty
+   | name = IDENT -> [name],CicAst.Implicit
+   ]
+  ];
   let_defs:[
     [ defs = LIST1 [
         name = IDENT;
-        args = LIST1 [
-            PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
-            SYMBOL ":"; ty = term; PAREN ")" ->
-              (names, Some ty)
-          | name = IDENT -> [name],None
-        ];
+        args = LIST1 [arg = arg -> arg];
         index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
         ty = OPT [ SYMBOL ":" ; t = term -> t ];
         SYMBOL <:unicode<def>> (* ≝ *);
@@ -196,12 +197,6 @@ EXTEND
                 list_of_binder binder ty 
                   (binder_of_arg_list binder final_term tl) l
           in
-          let args = 
-           List.map
-            (function
-                names,Some ty -> names,ty
-              | names,None -> names,CicAst.Implicit
-            ) args in
           let t1' = binder_of_arg_list `Lambda t1 args in
           let ty' = 
             match ty with 
@@ -457,9 +452,7 @@ EXTEND
     ]
   ];
   inductive_spec: [ [
-    fst_name = IDENT; params = LIST0 [
-      PAREN "("; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
-      typ = term; PAREN ")" -> (names, typ) ];
+    fst_name = IDENT; params = LIST0 [ arg=arg -> arg ];
     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
     fst_constructors = LIST0 constructor SEP SYMBOL "|";
     tl = OPT [ "with";