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),
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, HExtlib.Localized (_,exn)) ->
+ | Ploc.Exc (floc, HExtlib.Localized (_,exn)) ->
raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
- | Stdpp.Exc_located (floc, exn) ->
+ | Ploc.Exc (floc, exn) ->
raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
let parse_level1_pattern grammars precedence lexbuf =
args = LIST1 arg;
index_name = OPT [ "on"; id = single_arg -> id ];
ty = OPT [ SYMBOL ":" ; p = term -> p ];
- SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+ opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
let rec position_of name p = function
| [] -> None, p
| n :: _ when n = name -> Some p, p
name = single_arg;
args = LIST0 arg;
ty = OPT [ SYMBOL ":" ; p = term -> p ];
- SYMBOL <:unicode<def>> (* ≝ *); body = term ->
+ opt_body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
+ let body = match opt_body with Some body -> body | None -> Ast.Implicit `JustOne in
let args =
List.concat
(List.map