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 ())
]
];
[
[ "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>> (* ≝ *);
| 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 ->
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))))