The pretty printers in CicPp now have an optional ~metasenv argument to

[helm.git] / helm / software / components / cic_proof_checking / cicPp.mli

diff --git a/helm/software/components/cic_proof_checking/cicPp.mli b/helm/software/components/cic_proof_checking/cicPp.mli
index e84ae4fed1021f25d19e0025f01edbdefc1edd7b..e898c352d377a47c82d4cc11692fef79d6a6c950 100644 (file)
--- 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