X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicEnvironment.ml;h=8ae5c1b13c1a80a0cc9c974a05b71f8ccda6f49b;hb=08e9d02504942642a917c0d3e4b4795e65172d89;hp=314abf4eb99aa7a32fa4cfeeb8eeed561f3ecf60;hpb=59a1175d22ad8f7d0b225ed0c89c8b2f2d4dd276;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicEnvironment.ml b/helm/software/components/cic_proof_checking/cicEnvironment.ml
index 314abf4eb..8ae5c1b13 100644
--- a/helm/software/components/cic_proof_checking/cicEnvironment.ml
+++ b/helm/software/components/cic_proof_checking/cicEnvironment.ml
@@ -366,7 +366,7 @@ let get_object_to_add uri =
     match UriManager.bodyuri_of_uri uri with
        None -> None
     |  Some bodyuri ->
-        if Http_getter.exists' bodyuri then
+        if Http_getter.exists' ~local:false bodyuri then
           Some (Http_getter.getxml' bodyuri)
         else
           None
@@ -459,13 +459,13 @@ 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_ugraph ~increment:(u,uri)),l
+      o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),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_ugraph ~increment:(u,uri)),l
+        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))),l
     else
       (* we don't trust the uri, so we fail *)
       begin
@@ -493,14 +493,14 @@ let get_cooked_obj ?trust base_ugraph 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_ugraph ~increment:(u,uri)))
+    let o,u,l = Cache.find_cooked uri in
+      CheckedObj (o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*))))
   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 ~base_ugraph ~increment:(u,uri))
+      let o,u,l = add_trusted_uri_to_cache uri in
+        CheckedObj ( o, CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
     else
       let o,u,_ = find_or_add_to_unchecked uri in
       Cache.unchecked_to_frozen uri;
@@ -513,12 +513,12 @@ let is_type_checked ?(trust=true) base_ugraph 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_ugraph ~increment:(u,uri))
+    let o,u,l = Cache.find_cooked uri in
+      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... *)
-      let o,u,_ = find_or_add_to_unchecked uri in
-        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri))
+      let o,u,l = find_or_add_to_unchecked uri in
+        o,(CicUniv.merge_ugraphs ~base_ugraph ~increment:(u,uri(*,l*)))
 ;; 
 
 let in_cache uri =
@@ -527,7 +527,7 @@ let in_cache uri =
 let add_type_checked_obj uri (obj,ugraph,univlist) =
  Cache.add_cooked ~key:uri (obj,ugraph,univlist)
 
-let in_library uri = in_cache uri || Http_getter.exists' uri
+let in_library uri = in_cache uri || Http_getter.exists' ~local:false uri
 
 let remove_obj = Cache.remove