failwith msg
in
match style with
- | GrafiteAst.Declarative ->
+ | GrafiteAst.Declarative ->
let cobj = Acic2content.annobj2content ids_to_inner_sorts ids_to_inner_types aobj in
let bobj = Content2pres.content2pres ids_to_inner_sorts cobj in
remove_closed_substs ("\n\n" ^
BoxPp.render_to_string (function _::x::_ -> x | _ -> assert false) n (CicNotationPres.mpres_of_box bobj)
)
- | GrafiteAst.Procedural ->
+ | GrafiteAst.Procedural depth ->
let term_pp = term2pres (n - 8) ids_to_inner_sorts in
let lazy_term_pp = term_pp in
let obj_pp = CicNotationPp.pp_obj term_pp in
let aux = GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp in
let script = Acic2Procedural.acic2procedural
- ~ids_to_inner_sorts ~ids_to_inner_types prefix aobj in
+ ~ids_to_inner_sorts ~ids_to_inner_types ?depth prefix aobj in
"\n\n" ^ String.concat "" (List.map aux script)