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 +