Bug fixed: matitac used to stop too early when an ambigous identifier was met

and auto_disambiguation was true.

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index e286fb5502a3714087fe925a2181d1ce75cda81b..d2c11890fa7cf7ae4d61c88063124727f98bbd75 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -32,7 +32,11 @@ exception Ambiguous_input
 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