From 7ca56e8a1f819df077d544b890c49ae59fdf3aa7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 3 Feb 2006 10:07:38 +0000 Subject: [PATCH] default of auto_disambiguation set to true --- helm/ocaml/grafite_parser/grafiteDisambiguator.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 -- 2.39.5