X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=829e78b6d0d16476e4e73a968436c2774ec523b5;hb=95adf6dc8e29a71adc34e71eafe3f427990126e0;hp=117f0926e68a1913be2b75410af406f8ae007ccd;hpb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 117f0926e..829e78b6d 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -581,9 +581,9 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n
+    | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n
     | "Type" -> `Type (CicUniv.fresh ()) 
-    | "CProp"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NCProp n
+    | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
     | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];
@@ -712,7 +712,13 @@ EXTEND
   ];
   term: LEVEL "10"
   [
-    [ "let"; var = possibly_typed_name; SYMBOL <:unicode<def>> (* ≝ *);
+    [ "let"; 
+     var = 
+      [ 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<def>> (* ≝ *);
       p1 = term; "in"; p2 = term ->
         return_term loc (Ast.LetIn (var, p1, p2))
     | LETCOREC; defs = let_defs; "in";
@@ -750,7 +756,8 @@ EXTEND
       | 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)
+      | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
+      | SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
       | PLACEHOLDER -> return_term loc Ast.UserInput
       | m = META -> return_term loc (Ast.Meta (int_of_string m, []))
       | m = META; s = meta_substs ->
@@ -809,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))))