]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAstPp.mli
checked in new version of matita from svn
[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.mli
index f75e3f31709dbe2e8bedbaa9e049de82c894f556..f9fe2b2b8e4a362a7e7397039593ec4ed72a8c2c 100644 (file)
  *)
 
 val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string
-
-val pp_tactical:
-  (CicAst.term, string) TacticAst.tactic TacticAst.tactical ->
-    string
+val pp_command: CicAst.term TacticAst.command -> string
+val pp_macro: ('a -> string) -> 'a TacticAst.macro -> 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