new message reporting system improves performance significatively

[helm.git] / helm / software / helena / src / basic_rg / brgValidity.ml

diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml
index 18ec015df87e2b1c55dbdb4faf7fe792ad1b775d..e358d5a1909304faea2c84187ac0c9ed71ca14a0 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -11,13 +11,15 @@
 
 module L  = Log
 module E  = Entity
+module G  = Options
+module S  = Status
 module B  = Brg
 module BE = BrgEnvironment
 module BR = BrgReduction
 
 (* Internal functions *******************************************************)
 
-let level = 4
+let level = 3
 
 let message1 st1 m t1 =
    L.et_items1 "In the environment" m st1 t1
@@ -55,7 +57,7 @@ let assert_applicability err f st m v t =
       | _                                -> assert false (**)
 
 let rec b_validate err f st m x =
-   log1 "Now checking" m x;
+   if !G.trace >= level then log1 "Now checking" m x;
    match x with
    | B.Sort _         -> f ()
    | B.LRef (_, i)    ->
@@ -90,6 +92,4 @@ let rec b_validate err f st m x =
 
 (* Interface functions ******************************************************)
 
-and validate err f st m x =
-   let f () = L.unbox level; f () in
-   L.box level; b_validate err f st m x
+and validate err f st m x = b_validate err f st m x