A new switch to activate/deactive nCicReduction pretty printing.

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

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 5abd0139c920629d155e27ae3f4d9ecabf98dc91..ec97442ace47dfa50e3123ea6cee8f9b87fcfbb1 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -210,6 +210,11 @@ let _ =
     addDebugItem "disable refiner/unification logging"
       (fun _ -> NCicRefiner.debug := false; NCicUnification.debug := false;);
     addDebugSeparator ();
+    addDebugItem "enable reduction logging"
+      (fun _ -> NCicReduction.debug := true);
+    addDebugItem "disable reduction logging"
+      (fun _ -> NCicReduction.debug := false);
+    addDebugSeparator ();
     addDebugItem "Expand virtuals"
     (fun _ -> (MatitaScript.current ())#expandAllVirtuals);
   end