From: denes Date: Thu, 18 Jun 2009 11:01:08 +0000 (+0000) Subject: Changed parenthesis to optional around letin ident (and type) X-Git-Tag: make_still_working~3851 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b8e036c5f3f54406e36cee1177a78922d59a0295;p=helm.git Changed parenthesis to optional around letin ident (and type) --- diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index 117f0926e..7317f6139 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -712,7 +712,13 @@ EXTEND ]; term: LEVEL "10" [ - [ "let"; var = possibly_typed_name; SYMBOL <:unicode> (* ≝ *); + [ "let"; + var = + [ LPAREN; id = IDENT; SYMBOL ":"; typ = term; RPAREN -> + Ast.Ident(id,None), Some typ + | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] -> + Ast.Ident(id,None), ty ]; + SYMBOL <:unicode> (* ≝ *); p1 = term; "in"; p2 = term -> return_term loc (Ast.LetIn (var, p1, p2)) | LETCOREC; defs = let_defs; "in";