From cdd019ea6419fc058a92b1aca950a4eff11188d1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 8 Oct 2009 16:13:54 +0000 Subject: [PATCH] A new switch to activate/deactive nCicReduction pretty printing. --- helm/software/components/ng_kernel/nCicReduction.ml | 3 +++ helm/software/components/ng_kernel/nCicReduction.mli | 2 ++ helm/software/matita/matita.ml | 5 +++++ 3 files changed, 10 insertions(+) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index 2417f718b..717644ac5 100644 --- 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 9cff07d8f..713edd170 100644 --- 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 5abd0139c..ec97442ac 100644 --- 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 -- 2.39.2