X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fmatita.ml;h=d32f69cf01852512ce2c26e82afa4c8a23b44c84;hb=b33a11c031f1519628b0f90dc20df7e0507d5723;hp=7312602fa813490060bc47db3cfbd6d52e6adf2a;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index 7312602fa..d32f69cf0 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -93,9 +93,11 @@ let init_debugging_menu gui = addDebugSeparator (); addDebugCheckbox "tactics logging" (fun mi () -> NTacStatus.debug := mi#active); + addDebugCheckbox "disambiguation logging" + (fun mi () -> MultiPassDisambiguator.debug := mi#active; NCicDisambiguate.debug := mi#active); addDebugCheckbox "disambiguation/refiner/unification/metasubst logging" (fun mi () -> NCicRefiner.debug := mi#active; NCicUnification.debug := - mi#active; MultiPassDisambiguator.debug := mi#active; NCicMetaSubst.debug := mi#active); + mi#active; MultiPassDisambiguator.debug := mi#active; NCicDisambiguate.debug := mi#active; NCicMetaSubst.debug := mi#active); addDebugCheckbox "reduction logging" (fun mi () -> NCicReduction.debug := mi#active); addDebugSeparator ();