Universes speedup:

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

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 22845725ac05e983aec69d23bc133bd5265e2274..1f6789e76895156311b0cc7470f89fb1b8fb7813 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -452,17 +452,17 @@ let add_trusted_uri_to_cache uri =
 ;;
 
 (* get the uri, if we trust it will be added to the cacheOfCookedObjects *)
-let get_cooked_obj_with_univlist ?(trust=true) base_univ uri =
+let get_cooked_obj_with_univlist ?(trust=true) base_ugraph uri =
   try
     (* the object should be in the cacheOfCookedObjects *)
     let o,u,l = Cache.find_cooked uri in
-      o,(CicUniv.merge_ugraphs base_univ u),l
+      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l
   with Not_found ->
     (* this should be an error case, but if we trust the uri... *)
     if trust && trust_obj uri then
       (* trusting means that we will fetch cook it on the fly *)
       let o,u,l = add_trusted_uri_to_cache uri in
-        o,(CicUniv.merge_ugraphs base_univ u),l
+        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)),l
     else
       (* we don't trust the uri, so we fail *)
       begin
@@ -470,8 +470,8 @@ let get_cooked_obj_with_univlist ?(trust=true) base_univ uri =
         raise Not_found
       end
 
-let get_cooked_obj ?trust base_univ uri = 
-  let o,g,_ = get_cooked_obj_with_univlist ?trust base_univ uri in
+let get_cooked_obj ?trust base_ugraph uri = 
+  let o,g,_ = get_cooked_obj_with_univlist ?trust base_ugraph uri in
   o,g
       
 (* This has not the old semantic :( but is what the name suggests
@@ -488,16 +488,16 @@ let get_cooked_obj ?trust base_univ uri =
  * as the get_cooked_obj but returns a type_checked_obj
  *   
  *)
-let is_type_checked ?(trust=true) base_univ uri =
+let is_type_checked ?(trust=true) base_ugraph uri =
   try 
     let o,u,_ = Cache.find_cooked uri in
-      CheckedObj (o,(CicUniv.merge_ugraphs base_univ u))
+      CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri)))
   with Not_found ->
     (* this should return UncheckedObj *)
     if trust && trust_obj uri then
       (* trusting means that we will fetch cook it on the fly *)
       let o,u,_ = add_trusted_uri_to_cache uri in
-        CheckedObj ( o, CicUniv.merge_ugraphs u base_univ )
+        CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
     else
       let o,u,_ = find_or_add_to_unchecked uri in
       Cache.unchecked_to_frozen uri;
@@ -507,15 +507,15 @@ let is_type_checked ?(trust=true) base_univ uri =
 (* as the get cooked, but if not present the object is only fetched,
  * not unfreezed and committed 
  *)
-let get_obj base_univ uri =
+let get_obj base_ugraph uri =
   try
     (* the object should be in the cacheOfCookedObjects *)
     let o,u,_ = Cache.find_cooked uri in
-      o,(CicUniv.merge_ugraphs base_univ u)
+      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
   with Not_found ->
     (* this should be an error case, but if we trust the uri... *)
       let o,u,_ = find_or_add_to_unchecked uri in
-        o,(CicUniv.merge_ugraphs base_univ u)
+        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
 ;; 
 
 let in_cache uri =