From d5c4930c5eb92a76731f6fb3c19a2a0b8c268ba0 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jun 2005 16:11:00 +0000
Subject: [PATCH] New lighter syntax for "let rec".

---
 helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 3d7699ecd..fda6d14e6 100644
--- 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 
-- 
2.39.2