]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_proof_checking/cicPp.mli
ppterm added
[helm.git] / helm / ocaml / cic_proof_checking / cicPp.mli
index 99757d1862882d9eaa1542217539a29d77687ed6..8d9071fcc4aa77cae6c780d3a41eabc7bdeb4497 100644 (file)
@@ -39,3 +39,5 @@
 (* ppobj obj  returns a string with describing the cic object obj in a syntax *)
 (* similar to the one used by Coq                                             *)
 val ppobj : Cic.obj -> string
+
+val ppterm : Cic.term -> string