X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicPp.mli;h=371b75e29480e6b29678dbb8405aae3ebc4ec36d;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=99757d1862882d9eaa1542217539a29d77687ed6;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicPp.mli b/helm/ocaml/cic_proof_checking/cicPp.mli
index 99757d186..371b75e29 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.mli
+++ b/helm/ocaml/cic_proof_checking/cicPp.mli
@@ -39,3 +39,12 @@
 (* 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
+
+(* Required only by the topLevel. It is the generalization of ppterm to *)
+(* work with environments.                                              *)
+val pp : Cic.term -> (Cic.name option) list -> string
+
+val ppname : Cic.name -> string
+