From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 5 Feb 2004 13:29:41 +0000 (+0000)
Subject: added ( ) notation for binders
X-Git-Tag: V_0_2_3~48
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=740876f690817f05a14b40ee06455f97d3e0564c;p=helm.git

added ( ) notation for binders
---

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