]> matita.cs.unibo.it Git - helm.git/commitdiff
fixed usage of matita.auto_disambiguation
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 6 Feb 2006 09:40:31 +0000 (09:40 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 6 Feb 2006 09:40:31 +0000 (09:40 +0000)
matita/matitaGui.ml

index ed739eefbebb8c9be4a9e5ab95f919166625a722..34406a3cd147908ef96d76a9804ecafc3064815f 100644 (file)
@@ -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