added ( ) notation for binders

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 397d038678839f00941803ffa830c7c6af27d645..2bcbb88e8da8a984c5b29c77a4620cd5be539652 100644 (file)
--- 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