*)
val pp_tactic:
+ map_unicode_to_tex:bool ->
term_pp:('term -> string) ->
lazy_term_pp:('lazy_term -> string) ->
('term, 'lazy_term, 'term GrafiteAst.reduction, string)
string
val pp_tactic_pattern:
+ map_unicode_to_tex:bool ->
term_pp:('term -> string) ->
lazy_term_pp:('lazy_term -> string) ->
('term, 'lazy_term, string) GrafiteAst.pattern ->
term_pp:('term -> string) ->
obj_pp:('obj -> string) ->
('term,'obj) GrafiteAst.command -> string
-val pp_macro: term_pp:('term -> string) -> 'term GrafiteAst.macro -> string
+val pp_macro:
+ term_pp:('term -> string) ->
+ lazy_term_pp:('lazy_term -> string) ->
+ ('term,'lazy_term) GrafiteAst.macro -> string
val pp_comment:
+ map_unicode_to_tex:bool ->
term_pp:('term -> string) ->
lazy_term_pp:('lazy_term -> string) ->
obj_pp:('obj -> string) ->
string
val pp_executable:
+ map_unicode_to_tex:bool ->
term_pp:('term -> string) ->
lazy_term_pp:('lazy_term -> string) ->
obj_pp:('obj -> string) ->
obj_pp:('obj -> string) ->
('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string)
GrafiteAst.statement ->
+ map_unicode_to_tex:bool ->
string
-val pp_tactical:
+val pp_punctuation_tactical:
term_pp:('term -> string) ->
lazy_term_pp:('lazy_term -> string) ->
('term, 'lazy_term, 'term GrafiteAst.reduction, string)
- GrafiteAst.tactical ->
+ GrafiteAst.punctuation_tactical ->
string