urimanager removed

[helm.git] / matita / components / disambiguation / disambiguateTypes.ml

diff --git a/matita/components/disambiguation/disambiguateTypes.ml b/matita/components/disambiguation/disambiguateTypes.ml
index 23c16cff28e620e388f259c15e4bf6a44e0face4..f6e03d098ccd555de2bab69a0b4f41bb417cf4b5 100644 (file)
--- a/matita/components/disambiguation/disambiguateTypes.ml
+++ b/matita/components/disambiguation/disambiguateTypes.ml
@@ -73,14 +73,14 @@ type interactive_user_uri_choice_type =
   selection_mode:[`SINGLE | `MULTIPLE] ->
   ?ok:string ->
   ?enable_button_for_non_vars:bool ->
-  title:string -> msg:string -> id:string -> UriManager.uri list ->
-   UriManager.uri list
+  title:string -> msg:string -> id:string -> NReference.reference list ->
+   NReference.reference list
 
 type interactive_interpretation_choice_type = string -> int ->
   (Stdpp.location list * string * string) list list -> int list
 
 type input_or_locate_uri_type = 
-  title:string -> ?id:string -> unit -> UriManager.uri option
+  title:string -> ?id:string -> unit -> NReference.reference option
 
 let string_of_domain_item = function
   | Id s -> Printf.sprintf "ID(%s)" s