X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_unification%2FcoercGraph.ml;h=57274e616446b3dab7b416c8db8f71f3aace8441;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=fa18530e53cffdf37dca89171cfdc48433a85b1b;hpb=bb49c457d64878ed9611656f620548b5151e5dbd;p=helm.git

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index fa18530e5..57274e616 100644
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -31,14 +31,14 @@ let debug_print = if debug then prerr_endline else ignore
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion src tgt =
     try
-      let src = UriManager.uri_of_string (CicUtil.uri_of_term src) in
-      let tgt = UriManager.uri_of_string (CicUtil.uri_of_term tgt) in
+      let src = CicUtil.uri_of_term src in
+      let tgt = CicUtil.uri_of_term tgt in
       let l = 
         CoercDb.find_coercion 
           (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt) 
       in
       match l with
-      | [] -> prerr_endline ":( coercion non trovata"; None
+      | [] -> debug_print ":( coercion non trovata"; None
       | u::_ -> 
           debug_print (
             sprintf ":) TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" 
@@ -46,7 +46,7 @@ let look_for_coercion src tgt =
               (UriManager.name_of_uri src) 
               (UriManager.name_of_uri tgt)
               (UriManager.name_of_uri u));
-              Some (CicUtil.term_of_uri (UriManager.string_of_uri u))
+              Some (CicUtil.term_of_uri u)
     with Invalid_argument s -> 
       debug_print (":( coercion non trovata (fallita la uri_of_term): " ^ s);
       None
@@ -133,9 +133,7 @@ let close_coercion_graph src tgt uri =
           match l with
           | [] -> assert false 
           | he :: tl ->
-              let term_of_uri' uri = 
-                CicUtil.term_of_uri (UriManager.string_of_uri uri)
-              in
+              let term_of_uri' uri = CicUtil.term_of_uri uri in
               let first_step = 
                 Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [],
                   obj_attrs)