From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Sep 2005 09:46:26 +0000 (+0000)
Subject: Bug fixed: matitac used to stop too early when an ambigous identifier was met
X-Git-Tag: V_0_1_2_1~113
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=5f7a3378c923c055898496f6d134d82b0c5b6bfc;p=helm.git

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 e286fb550..d2c11890f 100644
--- 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