X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=6b5e3f8332c60e21283486461032d020f12ac60d;hb=cb7af66937e8c72ae6ea6694350a0c86f3e6ccf9;hp=2f9bb97a5d799dacfc8c3251c457d3001c19f4c8;hpb=8f8d3ad5a02faed2ddcaa22f49a9099175445ef4;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 2f9bb97a5..6b5e3f833 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -230,7 +230,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
           let cic =
             if is_uri ast then  (* we have the URI, build the term out of it *)
               try
-                CicUtil.term_of_uri name
+                CicUtil.term_of_uri (UriManager.uri_of_string name)
               with UriManager.IllFormedUri _ ->
                 CicTextualParser2.fail loc "Ill formed URI"
             else
@@ -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
              with exn ->
-               debug_print uri;
+               debug_print (UriManager.string_of_uri uri);
                debug_print (Printexc.to_string exn);
                assert false
             in