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<def>> (* ≝ *);
+    [ "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<def>> (* ≝ *);
       p1 = term; "in"; p2 = term ->
         return_term loc (Ast.LetIn (var, p1, p2))
     | LETCOREC; defs = let_defs; "in";