X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatita.ml;h=58b7de9f34c2a9f02d94b39cc0ac589e5d0ecc8d;hb=d62d1b28015b18a515bdf81e2a8f658d158fae5a;hp=5d22f85d579f8aa9f15b2e1e27a7ab061f1e8f5c;hpb=48b1c073868dcddf01140775cb0e5ac524fdbf14;p=helm.git

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 5d22f85d5..58b7de9f3 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -170,6 +170,11 @@ let _ =
         CicNotation.set_active_notations
           (List.map fst (CicNotation.get_all_notations ())));
     addDebugSeparator ();
+    addDebugItem "enable multiple disambiguation passes (default)"
+      (fun _ -> GrafiteDisambiguator.only_one_pass := false);
+    addDebugItem "enable only one disambiguation pass"
+      (fun _ -> GrafiteDisambiguator.only_one_pass := true);
+    addDebugSeparator ();
     addDebugItem "enable coercions hiding"
       (fun _ -> TermAcicContent.hide_coercions := true);
     addDebugItem "disable coercions hiding"