X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita.ml;h=58b7de9f34c2a9f02d94b39cc0ac589e5d0ecc8d;hb=55676f08ab60b802d00ed47e8089d8622bc3dadb;hp=5d22f85d579f8aa9f15b2e1e27a7ab061f1e8f5c;hpb=d3f5be46ea4f2cee636e2e64c36a82f0dd5f51a9;p=helm.git diff --git a/matita/matita.ml b/matita/matita.ml index 5d22f85d5..58b7de9f3 100644 --- a/matita/matita.ml +++ b/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"