(* 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"
(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
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)