many strings that are supposed to be URIs are now UriManager.uri

[helm.git] / helm / matita / matitaDisambiguator.ml

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index f6db501b3f456267cff48818c395f8f722a2e98d..e286fb5502a3714087fe925a2181d1ce75cda81b 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -29,7 +29,7 @@ open MatitaTypes
 
 exception Ambiguous_input
 
-type choose_uris_callback = id:string -> string list -> string list
+type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
 type choose_interp_callback = (string * string) list list -> int list
 
 let mono_uris_callback ~id = raise Ambiguous_input