*)
val pp_tactic:
- (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string)
+ term_pp:('term -> string) ->
+ lazy_term_pp:('lazy_term -> string) ->
+ ('term, 'lazy_term, 'term GrafiteAst.reduction, string)
GrafiteAst.tactic ->
string
-val pp_command:
- (CicNotationPt.term,CicNotationPt.obj) GrafiteAst.command -> string
-val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string
+val pp_tactic_pattern:
+ term_pp:('term -> string) ->
+ lazy_term_pp:('lazy_term -> string) ->
+ ('term, 'lazy_term, string) GrafiteAst.pattern ->
+ string
+
+val pp_reduction_kind:
+ term_pp:('a -> string) ->
+ 'a GrafiteAst.reduction ->
+ string
+val pp_command: obj_pp:('obj -> string) -> 'obj GrafiteAst.command -> string
+val pp_macro: term_pp:('term -> string) -> 'term GrafiteAst.macro -> string
val pp_comment:
- (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
- CicNotationPt.obj, string)
+ term_pp:('term -> string) ->
+ lazy_term_pp:('lazy_term -> string) ->
+ obj_pp:('obj -> string) ->
+ ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string)
GrafiteAst.comment ->
string
val pp_executable:
- (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
- CicNotationPt.obj, string)
+ term_pp:('term -> string) ->
+ lazy_term_pp:('lazy_term -> string) ->
+ obj_pp:('obj -> string) ->
+ ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string)
GrafiteAst.code ->
string
val pp_statement:
- (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction,
- CicNotationPt.obj, string)
+ term_pp:('term -> string) ->
+ lazy_term_pp:('lazy_term -> string) ->
+ obj_pp:('obj -> string) ->
+ ('term, 'lazy_term, 'term GrafiteAst.reduction, 'obj, string)
GrafiteAst.statement ->
string
-val pp_macro_ast: CicNotationPt.term GrafiteAst.macro -> string
-val pp_macro_cic: Cic.term GrafiteAst.macro -> string
-
val pp_tactical:
- (CicNotationPt.term, CicNotationPt.term, CicNotationPt.term GrafiteAst.reduction, string)
+ term_pp:('term -> string) ->
+ lazy_term_pp:('lazy_term -> string) ->
+ ('term, 'lazy_term, 'term GrafiteAst.reduction, string)
GrafiteAst.tactical ->
string
-val pp_alias: GrafiteAst.alias_spec -> string
-
-val pp_cic_command: (Cic.term,Cic.obj) GrafiteAst.command -> string
-
-val pp_dependency: GrafiteAst.dependency -> string
-