From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 3 Feb 2006 10:07:38 +0000 (+0000)
Subject: default of auto_disambiguation set to true
X-Git-Tag: make_still_working~7659
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ca56e8a1f819df077d544b890c49ae59fdf3aa7;p=helm.git

default of auto_disambiguation set to true
---

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguator.ml b/helm/ocaml/grafite_parser/grafiteDisambiguator.ml
index d05351cd2..abe8c1de1 100644
--- a/helm/ocaml/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguator.ml
@@ -40,7 +40,9 @@ type choose_uris_callback =
 type choose_interp_callback = (string * string) list list -> int list
 
 let mono_uris_callback ~id =
- if Helm_registry.get_bool "matita.auto_disambiguation" then
+ if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
+      "matita.auto_disambiguation"
+ then
   function l -> l
  else
   raise Ambiguous_input