From 09cfd99de377d72d7af96ad9815342a1b7b467a9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Sep 2009 14:41:47 +0000 Subject: [PATCH] allow @{ ... } as the identifier of the letin --- helm/software/components/content_pres/cicNotationParser.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index af9edd9be..1a664d525 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -714,8 +714,8 @@ EXTEND [ [ "let"; var = - [ LPAREN; id = IDENT; SYMBOL ":"; typ = term; RPAREN -> - Ast.Ident(id,None), Some typ + [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN -> + id, Some typ | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] -> Ast.Ident(id,None), ty ]; SYMBOL <:unicode> (* ≝ *); @@ -816,6 +816,8 @@ let exc_located_wrapper f = with | Stdpp.Exc_located (floc, Stream.Error msg) -> raise (HExtlib.Localized (floc, Parse_error msg)) + | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) -> + raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn)))) | Stdpp.Exc_located (floc, exn) -> raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn)))) -- 2.39.2