Changed parenthesis to optional around letin ident (and type)

[helm.git] / helm / software / components / content_pres / cicNotationParser.ml

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index bb3d29f069d336544546c1a22e86fbdfc9a71f4c..7317f6139b0bf96e8ec4d8595b51e72d6d1ced6e 100644 (file)
--- 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";
@@ -748,6 +754,7 @@ EXTEND
           return_term loc (Ast.Ident (id, Some s))
       | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
       | u = URI -> return_term loc (Ast.Uri (u, None))
+      | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
       | n = NUMBER -> return_term loc (Ast.Num (n, 0))
       | IMPLICIT -> return_term loc (Ast.Implicit)
       | PLACEHOLDER -> return_term loc Ast.UserInput