X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=2bcbb88e8da8a984c5b29c77a4620cd5be539652;hb=740876f690817f05a14b40ee06455f97d3e0564c;hp=397d038678839f00941803ffa830c7c6af27d645;hpb=d8a1a68b8b7e53ba43fcad55e928a99ef5e08b8e;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 397d03867..2bcbb88e8 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -109,8 +109,13 @@ EXTEND
       ]
     | "binder" RIGHTA
       [
-        b = binder; vars = LIST1 IDENT SEP SYMBOL ",";
-        typ = OPT [ SYMBOL ":"; t = term -> t ];
+        b = binder;
+        (vars, typ) =
+          [ vars = LIST1 IDENT SEP SYMBOL ",";
+            typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
+          | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
+            typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
+          ];
         SYMBOL "."; body = term ->
           let binder =
             List.fold_right