From b8e036c5f3f54406e36cee1177a78922d59a0295 Mon Sep 17 00:00:00 2001
From: denes <??>
Date: Thu, 18 Jun 2009 11:01:08 +0000
Subject: [PATCH] Changed parenthesis to optional around letin ident (and type)

---
 .../software/components/content_pres/cicNotationParser.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

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";
-- 
2.39.2