From 740876f690817f05a14b40ee06455f97d3e0564c Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 5 Feb 2004 13:29:41 +0000 Subject: [PATCH] added ( ) notation for binders --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) 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 -- 2.39.2