X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicPp.mli;h=e898c352d377a47c82d4cc11692fef79d6a6c950;hb=d025518bc5930796c748704b069a2719b34b00d3;hp=e84ae4fed1021f25d19e0025f01edbdefc1edd7b;hpb=55b82bd235d82ff7f0a40d980effe1efde1f5073;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicPp.mli b/helm/software/components/cic_proof_checking/cicPp.mli
index e84ae4fed..e898c352d 100644
--- a/helm/software/components/cic_proof_checking/cicPp.mli
+++ b/helm/software/components/cic_proof_checking/cicPp.mli
@@ -40,13 +40,13 @@
 (* similar to the one used by Coq                                            *)
 val ppobj : Cic.obj -> string
 
-val ppterm : Cic.term -> string
+val ppterm : ?metasenv:Cic.metasenv -> Cic.term -> string
 
-val ppcontext : ?sep:string -> Cic.context -> string 
+val ppcontext : ?metasenv:Cic.metasenv -> ?sep:string -> Cic.context -> 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 pp : ?metasenv:Cic.metasenv -> Cic.term -> (Cic.name option) list -> string
 
 val ppname : Cic.name -> string