maxipatch for support of multiple DBs.

[helm.git] / components / tactics / closeCoercionGraph.ml

diff --git a/components/tactics/closeCoercionGraph.ml b/components/tactics/closeCoercionGraph.ml
index 898946ad64f6d89e77c0b18900644c55b0b8462c..d9dc679b32c35c85cafd5b25b68c66f45df554e3 100644 (file)
--- a/components/tactics/closeCoercionGraph.ml
+++ b/components/tactics/closeCoercionGraph.ml
@@ -316,8 +316,8 @@ let number_if_already_defined buri name l =
     if List.exists (UriManager.eq uri) l then retry ()
     else
       try
-        let _  = Http_getter.resolve' ~writable:true uri in
-        if Http_getter.exists' uri then retry () else uri
+        let _  = Http_getter.resolve' ~local:true ~writable:true uri in
+        if Http_getter.exists' ~local:true uri then retry () else uri
       with 
       | Http_getter_types.Key_not_found _ -> uri
       | Http_getter_types.Unresolvable_URI _ -> assert false
@@ -357,8 +357,7 @@ let close_coercion_graph src tgt uri baseuri =
                             [] [] univ arity true
                         in
                         if (menv = []) then
-                          prerr_endline 
-                            "MENV non empty after composing coercions";
+                          HLog.warn "MENV non empty after composing coercions";
                         build_obj t univ arity
                     | _ -> assert false 
                   ) (first_step, CicUniv.empty_ugraph) tl