X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=8014a19404d99da98716962b039b203ef559e97d;hb=b1bd861e3aaeef9e65ce1d35e5ae7d8db5f0d0e9;hp=22138dde8d1eee672f46385db7bc68f9428c29d7;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 22138dde8..8014a1940 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -303,17 +303,17 @@ let find_or_add_unchecked_to_cache uri =
  Cache.find_or_add_unchecked uri
   ~get_object_to_add:
    (function () ->
-     let filename = Getter.getxml uri in
+     let filename = Http_getter.getxml' uri in
      let bodyfilename =
       match UriManager.bodyuri_of_uri uri with
          None -> None
        | Some bodyuri ->
           try
-           ignore (Getter.resolve bodyuri) ;
+           ignore (Http_getter.resolve' bodyuri) ;
            (* The body exists ==> it is not an axiom *)
-           Some (Getter.getxml bodyuri)
+           Some (Http_getter.getxml' bodyuri)
           with
-           Getter.Unresolved ->
+           Http_getter_types.Unresolvable_URI _ ->
             (* The body does not exist ==> we consider it an axiom *)
             None
      in
@@ -399,3 +399,9 @@ let put_inductive_definition uri obj =
     Cic.InductiveDefinition _ -> Cache.add_cooked uri obj
   | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed
 ;;
+
+let in_cache uri = 
+ try
+  ignore (Cache.find_cooked uri);true
+ with Not_found -> false
+;;