* http://helm.cs.unibo.it/
*)
-val pp_tactic: (CicNotationPt.term, string) GrafiteAst.tactic -> string
+val pp_tactic:
+ (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, string)
+ GrafiteAst.tactic ->
+ string
+
val pp_obj: GrafiteAst.obj -> string
val pp_command: (CicNotationPt.term,GrafiteAst.obj) GrafiteAst.command -> string
+val pp_metadata: GrafiteAst.metadata -> string
val pp_macro: ('a -> string) -> 'a GrafiteAst.macro -> string
-val pp_comment: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.comment -> string
-val pp_executable: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.code -> string
-val pp_statement: (CicNotationPt.term,GrafiteAst.obj,string) GrafiteAst.statement -> string
+
+val pp_comment:
+ (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj,
+ string)
+ GrafiteAst.comment ->
+ string
+
+val pp_executable:
+ (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj,
+ string)
+ GrafiteAst.code ->
+ string
+
+val pp_statement:
+ (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.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, string) GrafiteAst.tactical -> string
+
+val pp_tactical:
+ (CicNotationPt.term, CicNotationPt.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
+
+val pp_cic_appl_pattern: CicNotationPt.cic_appl_pattern -> string
+