]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_proof_checking/cicPp.mli
New experimental commit: metavariables representation is changed again,
[helm.git] / helm / ocaml / cic_proof_checking / cicPp.mli
index afc519c9f3ea43ab21f30d80aa0a4c76c1b2adb5..9f68d0525200a0ba959aee302bdd969d47752ca1 100644 (file)
@@ -44,4 +44,4 @@ 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
+val pp : Cic.term -> (Cic.name option) list -> string