From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 16 Apr 2002 11:40:51 +0000 (+0000)
Subject: pp exported
X-Git-Tag: V_0_3_0_debian_8~146
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=489679090cdd70dfd1ad57e681970fd6f0b6e6f9;p=helm.git

pp exported
---

diff --git a/helm/ocaml/cic_proof_checking/cicPp.mli b/helm/ocaml/cic_proof_checking/cicPp.mli
index 8d9071fcc..afc519c9f 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.mli
+++ b/helm/ocaml/cic_proof_checking/cicPp.mli
@@ -41,3 +41,7 @@
 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 list -> string