X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=2bcbb88e8da8a984c5b29c77a4620cd5be539652;hb=0ce5aa521e96d3885cfdede3c31acb7bbb371029;hp=397d038678839f00941803ffa830c7c6af27d645;hpb=7aee283a4fee4fca3fc1d53619c366f793f1e694;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