A new switch to activate/deactive nCicReduction pretty printing.

diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml
index 2417f718b8e4576fca9ffc16a6024a456a615e1c..717644ac558d170a6b31d999e85a75cb3cd61e84 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.ml
+++ b/helm/software/components/ng_kernel/nCicReduction.ml
@@ -17,6 +17,9 @@ module E = NCicEnvironment
 
 exception AssertFailure of string Lazy.t;;
 
+let debug = ref false;;
+let pp m = if !debug then prerr_endline (Lazy.force m) else ();;
+
 module type Strategy = sig
   type stack_term
   type env_term

diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli
index 9cff07d8fd0b9e623245f12ab6cdf09d24936bcf..713edd1705050d14fe6ee2d1fee270a71f7fd713 100644 (file)
--- a/helm/software/components/ng_kernel/nCicReduction.mli
+++ b/helm/software/components/ng_kernel/nCicReduction.mli
@@ -13,6 +13,8 @@
 
 exception AssertFailure of string Lazy.t;;
 
+val debug: bool ref
+
 val whd : 
   ?delta:int -> subst:NCic.substitution -> 
   NCic.context -> NCic.term -> 

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