default of auto_disambiguation set to true

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguator.ml b/helm/ocaml/grafite_parser/grafiteDisambiguator.ml
index d05351cd240630587b08d9f179017c859e3e949a..abe8c1de1f75373c33fbfdf018eaaf3984d4c785 100644 (file)
--- 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