X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FcloseCoercionGraph.ml;h=d9dc679b32c35c85cafd5b25b68c66f45df554e3;hb=111df95ac03f2ee21dfa2422a7f531f675b1c16d;hp=898946ad64f6d89e77c0b18900644c55b0b8462c;hpb=32e29e1be132c4f9453787a194314ed57aa18538;p=helm.git

diff --git a/helm/software/components/tactics/closeCoercionGraph.ml b/helm/software/components/tactics/closeCoercionGraph.ml
index 898946ad6..d9dc679b3 100644
--- a/helm/software/components/tactics/closeCoercionGraph.ml
+++ b/helm/software/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