From 5f7a3378c923c055898496f6d134d82b0c5b6bfc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 5 Sep 2005 09:46:26 +0000 Subject: [PATCH] Bug fixed: matitac used to stop too early when an ambigous identifier was met and auto_disambiguation was true. --- helm/matita/matitaDisambiguator.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 -- 2.39.2