From 489679090cdd70dfd1ad57e681970fd6f0b6e6f9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 16 Apr 2002 11:40:51 +0000 Subject: [PATCH] pp exported --- helm/ocaml/cic_proof_checking/cicPp.mli | 4 ++++ 1 file changed, 4 insertions(+) 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 -- 2.39.2