From d39571d4fed32b6db8c355189bb099e2837eaf9c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 6 Feb 2006 09:40:31 +0000 Subject: [PATCH] fixed usage of matita.auto_disambiguation --- helm/software/matita/matitaGui.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index ed739eefb..34406a3cd 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -1133,7 +1133,7 @@ let interactive_uri_choice let gui = instance () in let nonvars_uris = lazy (List.filter (non UriManager.uri_is_var) uris) in if (selection_mode <> `SINGLE) && - (Helm_registry.get_bool "matita.auto_disambiguation") + (Helm_registry.get_opt_default Helm_registry.get_bool ~default:true "matita.auto_disambiguation") then Lazy.force nonvars_uris else begin -- 2.39.5