From 6b2ff99f3f6cd0e46166bc05d06eb7421f7fda84 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jun 2005 16:19:14 +0000 Subject: [PATCH] New syntax (again) for let rec binders: let rec f x y (z,w:T) h (c:T) = ... --- helm/ocaml/cic_disambiguation/cicTextualParser2.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index fda6d14e6..e267aff6a 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -175,9 +175,10 @@ EXTEND [ defs = LIST1 [ name = IDENT; args = LIST1 [ - PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; - ty = OPT [ SYMBOL ":"; ty = term -> ty ] ; PAREN ")" -> - (names, ty) + PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; + SYMBOL ":"; ty = term; PAREN ")" -> + (names, Some ty) + | name = IDENT -> [name],None ]; index_name = OPT [ IDENT "on"; idx = IDENT -> idx ]; ty = OPT [ SYMBOL ":" ; t = term -> t ]; -- 2.39.2