match magic with
| Ast.List0 (_, None) -> Gramext.Slist0 s
| Ast.List1 (_, None) -> Gramext.Slist1 s
- | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l)
- | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l)
+ | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l, false)
+ | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l, false)
| _ -> assert false
in
[ Env (List.map Env.list_declaration p_names),
| [],[] -> 0
| [],_ -> ~-1
| _,[] -> 1
- | ((s1::tl1) as x),((s2::tl2) as y) ->
+ | ((s1::tl1) ),((s2::tl2) ) ->
if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
- else Pervasives.compare x y
+ else
+ let res =
+ try Pervasives.compare s1 s2
+ with Invalid_argument _ -> 0
+ in
+ if res = 0 then aux (tl1, tl2) else res
in
aux (x,y)
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>> (* ≝ *);
try
f ()
with
- | Stdpp.Exc_located (floc, Stream.Error msg) ->
+ | Ploc.Exc (floc, Stream.Error msg) ->
raise (HExtlib.Localized (floc, Parse_error msg))
- | Stdpp.Exc_located (floc, exn) ->
+ | Ploc.Exc (floc, HExtlib.Localized (_,exn)) ->
+ raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
+ | Ploc.Exc (floc, exn) ->
raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
let parse_level1_pattern precedence lexbuf =