New syntax (again) for let rec binders:

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 78d1bf181c8b99c1d14b965244eac25eacc7ebc0..e267aff6a28ed9324c953f35d9f39aa535b45903 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -175,9 +175,10 @@ EXTEND
     [ defs = LIST1 [
         name = IDENT;
         args = LIST1 [
-          PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
-          ty = term; PAREN ")" ->
-            (names, ty)
+            PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
+            SYMBOL ":"; ty = term; PAREN ")" ->
+              (names, Some ty)
+          | name = IDENT -> [name],None
         ];
         index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
         ty = OPT [ SYMBOL ":" ; t = term -> t ];
@@ -195,6 +196,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 
@@ -377,8 +384,8 @@ EXTEND
     | [ IDENT "intro" ] ->
         TacticAst.Intros (loc, Some 1, [])
     | [ IDENT "left" ] -> TacticAst.Left loc
-    | [ "let" | "Let" ];
-      t = tactic_term; "in"; where = IDENT ->
+    | [ IDENT "letin" ];
+       where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
         TacticAst.LetIn (loc, t, where)
     | kind = reduction_kind;
       pat = OPT [