]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.ml
many strings that are supposed to be URIs are now UriManager.uri
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml
index 2f9bb97a5d799dacfc8c3251c457d3001c19f4c8..27122ef1deaf635f594d2931d2a606046fc81069 100644 (file)
@@ -622,7 +622,7 @@ module Make (C: Callbacks) =
       let uris =
        match uris with
         | [] ->
-           [UriManager.string_of_uri (C.input_or_locate_uri
+           [(C.input_or_locate_uri
             ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
         | [uri] -> [uri]
         | _ ->
@@ -635,12 +635,12 @@ module Make (C: Callbacks) =
       in
       List.map
         (fun uri ->
-          (uri,
+          (UriManager.string_of_uri uri,
            let term =
              try
-               CicUtil.term_of_uri uri
+               CicUtil.term_of_uri (UriManager.string_of_uri uri)
              with exn ->
-               debug_print uri;
+               debug_print (UriManager.string_of_uri uri);
                debug_print (Printexc.to_string exn);
                assert false
             in