let rec/corec and co/inductive are not printed!

[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 2ac6b7e6a4ad31e702b9c58768c09f7effcd50d2..1a664d525d82018672d727548b807e3bf3232c83 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -714,8 +714,8 @@ EXTEND
   [
     [ "let"; 
      var = 
-      [ LPAREN; id = IDENT; SYMBOL ":"; typ = term; RPAREN ->
-         Ast.Ident(id,None), Some typ
+      [ 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>> (* ≝ *);
@@ -757,7 +757,7 @@ EXTEND
       | 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 `JustOne)
-      | IMPLICITVECTOR -> return_term loc (Ast.Implicit `Vector)
+      | 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 ->
@@ -816,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))))