X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.mli;h=55566a614493de9ae8b872a0a9347d2cf6a37073;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=4490e6586eba94ec42b11dfc3a836961536893e1;hpb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index 4490e6586..55566a614 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -36,7 +36,7 @@
 (*                                                                          *)
 (****************************************************************************)
 
-exception CircularDependency of string;;
+exception CircularDependency of string Lazy.t;;
 exception Object_not_found of UriManager.uri;;
 
 (* as the get cooked, but if not present the object is only fetched,
@@ -77,13 +77,16 @@ val is_type_checked :
 (* see the .ml file for some reassuring invariants                    *)
 (* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
 val set_type_checking_info : 
-  ?replace_ugraph:(CicUniv.universe_graph option) -> UriManager.uri -> unit
+  ?replace_ugraph_and_univlist:
+    ((CicUniv.universe_graph * CicUniv.universe list) option) -> 
+    UriManager.uri -> unit
 
 (* this function is called by CicTypeChecker.typecheck_obj to add to the *)
 (* environment a new well typed object that is not yet in the library    *)
 (* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
 val add_type_checked_obj : 
-  UriManager.uri -> (Cic.obj * CicUniv.universe_graph) -> unit
+  UriManager.uri -> 
+  (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> unit
 
   (** remove a type checked object
   * @raise Object_not_found when given term is not in the environment
@@ -98,6 +101,14 @@ val get_cooked_obj :
   ?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->
     Cic.obj * CicUniv.universe_graph
 
+(* get_cooked_obj_with_univlist ~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) *)
+(* Otherwise it raises Not_found                                    *)
+val get_cooked_obj_with_univlist : 
+  ?trust:bool -> CicUniv.universe_graph -> UriManager.uri ->
+    Cic.obj * CicUniv.universe_graph * CicUniv.universe list
+
 (* FUNCTIONS USED ONLY IN THE TOPLEVEL/PROOF-ENGINE *)
 
 (* (de)serialization *)