New lighter syntax for "let rec".

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 3d7699ecde14207b2d3e7ad4410321d927f1076a..fda6d14e636eac74aefc6da73e0b6a22d7dda114 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -175,8 +175,8 @@ EXTEND
     [ defs = LIST1 [
         name = IDENT;
         args = LIST1 [
-          PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
-          ty = term; PAREN ")" ->
+          PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
+          ty = OPT [ SYMBOL ":"; ty = term -> ty ] ; PAREN ")" ->
             (names, ty)
         ];
         index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
@@ -195,6 +195,12 @@ 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