new universes implementation

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.mli

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index 615cdf9be37675fbab987ce27bb3257dcba8221f..e3def568e4bdeba80ae3b4ad147ed05eb6deaba2 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -61,6 +61,9 @@ val is_type_checked : ?trust:bool -> UriManager.uri -> type_checked_obj
 (* again in the future (is_type_checked will return true)             *)
 val set_type_checking_info : UriManager.uri -> unit
 
+(* We need this in the Qed. *)
+val add_type_checked_term : UriManager.uri -> Cic.obj -> unit
+
 (* get_cooked_obj ~trust uri                                        *)
 (* returns the object if it is already type-checked or if it can be *)
 (* trusted (if [trust] = true and the trusting function accepts it) *)