Main result for e.

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

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index a326754dc40a39ac65ad30df18e795f4d64eae95..60b112d982cca6bf9e6c75ae77d935d6f3114195 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -233,6 +233,10 @@ let _ =
       (fun _ -> GrafiteDisambiguator.only_one_pass := false);
     addDebugItem "enable only one disambiguation pass"
       (fun _ -> GrafiteDisambiguator.only_one_pass := true);
+    addDebugItem "always show all disambiguation errors"
+      (fun _ -> MatitaGui.all_disambiguation_passes := true);
+    addDebugItem "prune disambiguation errors"
+      (fun _ -> MatitaGui.all_disambiguation_passes := false);
     addDebugSeparator ();
 (* ZACK moved to the View menu
     addDebugItem "enable coercions hiding"