prima implementazione di demodulate, superposition_left e superposition_right

[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.mli

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli
index 356b07e76f6ca87e1a154c87024f3156d499ae12..3308adf924c0bc2dbbd82d1423c18e1a4cd3366b 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.mli
+++ b/helm/ocaml/cic_transformations/tacticAstPp.mli
@@ -24,6 +24,13 @@
  *)
 
 val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string
-
+val pp_command: CicAst.term 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_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