X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAstPp.mli;h=fb9b45084ee7a584174ee0e2321b9c5a380a5ce1;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=f75e3f31709dbe2e8bedbaa9e049de82c894f556;hpb=f065a68682b23976d185370d85869c196da3f20b;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli
index f75e3f317..fb9b45084 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.mli
+++ b/helm/ocaml/cic_transformations/tacticAstPp.mli
@@ -24,8 +24,15 @@
  *)
 
 val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string
+val pp_obj: TacticAst.obj -> string
+val pp_command: (CicAst.term,TacticAst.obj) TacticAst.command -> string
+val pp_macro: ('a -> string) -> 'a TacticAst.macro -> string
+val pp_comment: (CicAst.term,TacticAst.obj,string) TacticAst.comment -> string
+val pp_executable: (CicAst.term,TacticAst.obj,string) TacticAst.code -> string
+val pp_statement: (CicAst.term,TacticAst.obj,string) TacticAst.statement -> string
+val pp_macro_ast: CicAst.term TacticAst.macro -> string
+val pp_macro_cic: Cic.term TacticAst.macro -> string
+val pp_tactical: (CicAst.term, string) TacticAst.tactical -> string
+val pp_alias: TacticAst.alias_spec -> string
 
-val pp_tactical:
-  (CicAst.term, string) TacticAst.tactic TacticAst.tactical ->
-    string
-
+val pp_cic_command: (Cic.term,Cic.obj) TacticAst.command -> string