From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 8 Jun 2005 16:11:00 +0000 (+0000)
Subject: New lighter syntax for "let rec".
X-Git-Tag: PRE_INDEX_1~32
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d5c4930c5eb92a76731f6fb3c19a2a0b8c268ba0;p=helm.git

New lighter syntax for "let rec".
---

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