]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAstPp.mli
New function (only partially implemented) to pretty print an Ast at the
[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.mli
index d4cae4405ed66550d4fb159e250d5499bcfce9c1..fb9b45084ee7a584174ee0e2321b9c5a380a5ce1 100644 (file)
@@ -35,3 +35,4 @@ 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_cic_command: (Cic.term,Cic.obj) TacticAst.command -> string