X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.ml;h=60b112d982cca6bf9e6c75ae77d935d6f3114195;hb=c38c15fa800498bcac6230e07a31ed54414a0865;hp=a326754dc40a39ac65ad30df18e795f4d64eae95;hpb=5da42f6120f3075c3da8ab3082ead39ea57955fa;p=helm.git

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index a326754dc..60b112d98 100644
--- 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"