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 4b94226cbe2ae63f2c94ee85eb12d85ed9dfaa4d..9510287450ce9398b46e6069387480e6f30b7282 100644 (file)
--- 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";