new disambiguator almost attached

[helm.git] / helm / software / matita / matita.ml

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index d63e327f03b89e8d68a58b7ce2a80e68e945ff78..247e07d7a7912ac7652e7e282ca7a8c3fa0626e2 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -236,9 +236,9 @@ let _ =
 *)
     addDebugSeparator ();
     addDebugItem "enable multiple disambiguation passes (default)"
-      (fun _ -> GrafiteDisambiguator.only_one_pass := false);
+      (fun _ -> MultiPassDisambiguator.only_one_pass := false);
     addDebugItem "enable only one disambiguation pass"
-      (fun _ -> GrafiteDisambiguator.only_one_pass := true);
+      (fun _ -> MultiPassDisambiguator.only_one_pass := true);
     addDebugItem "always show all disambiguation errors"
       (fun _ -> MatitaGui.all_disambiguation_passes := true);
     addDebugItem "prune disambiguation errors"