X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAstPp.mli;h=d4cae4405ed66550d4fb159e250d5499bcfce9c1;hb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;hp=3308adf924c0bc2dbbd82d1423c18e1a4cd3366b;hpb=53ee2f5095adadffcafb40e436d23dc330d3bd87;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli
index 3308adf92..d4cae4405 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.mli
+++ b/helm/ocaml/cic_transformations/tacticAstPp.mli
@@ -24,11 +24,12 @@
  *)
 
 val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string
-val pp_command: CicAst.term TacticAst.command -> 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,string) TacticAst.comment -> string
-val pp_executable: (CicAst.term,string) TacticAst.code -> string
-val pp_statement: (CicAst.term,string) TacticAst.statement -> 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