version 0.7.1

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

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index fcbcdea1442cce3be7be508881038f0599ebbce6..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
@@ -63,3 +63,4 @@ module Disambiguator = Disambiguate.Make (Callbacks)
 
 let disambiguate_term = Disambiguator.disambiguate_term
 
+let disambiguate_obj = Disambiguator.disambiguate_obj