more strings to UriManager.uri

[helm.git] / helm / ocaml / cic_unification / coercGraph.ml

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index fa18530e53cffdf37dca89171cfdc48433a85b1b..c1056b6eca8a912c1ba9b0171ebcf368ea514a3a 100644 (file)
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -31,8 +31,8 @@ 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) 
@@ -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)