X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaDisambiguator.ml;h=d2c11890fa7cf7ae4d61c88063124727f98bbd75;hb=513e52fa53da03a4775d9a6bc3c93eafb5f3f9df;hp=f6db501b3f456267cff48818c395f8f722a2e98d;hpb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;p=helm.git

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index f6db501b3..d2c11890f 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -29,10 +29,14 @@ 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
+let mono_uris_callback ~id =
+ if Helm_registry.get_bool "matita.auto_disambiguation" then
+  function l -> l
+ else
+  raise Ambiguous_input
 let mono_interp_callback _ = raise Ambiguous_input
 
 let _choose_uris_callback = ref mono_uris_callback