X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcoercGraph.ml;h=57274e616446b3dab7b416c8db8f71f3aace8441;hb=0f3081bec320860fbe2208e4d3314629e12a320f;hp=d7454925a606f8a0ddd93fa9bc112a070dcbb240;hpb=6376b9d56df8c0151a4cd5f35f2646d9922b5858;p=helm.git

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index d7454925a..57274e616 100644
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -25,20 +25,20 @@
 
 open Printf;;
 
-let debug = true
+let debug = false
 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)