From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 6 Feb 2006 09:40:31 +0000 (+0000)
Subject: fixed usage of matita.auto_disambiguation
X-Git-Tag: 0.4.95@7852~1727
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7906a230a7989fab555d50ae930bb4169cb5d631;hp=b86caba4f52e441e0456f7afa404750ff0ba1109;p=helm.git

fixed usage of matita.auto_disambiguation
---

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index ed739eefb..34406a3cd 100644
--- a/matita/matitaGui.ml
+++ b/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