- conditional compilation continues ...

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

diff --git a/helm/software/helena/src/basic_rg/brgType.ml b/helm/software/helena/src/basic_rg/brgType.ml
index 7cdeb653a99f27154a7b252fd36e6a1e8d3c7f89..431e3e4737f3676452aae3fb5e74d9d287e8fc2c 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -22,6 +22,8 @@ module BE = BrgEnvironment
 module BS = BrgSubstitution
 module BR = BrgReduction
 
+IFDEF TYPE THEN
+
 (* Internal functions *******************************************************)
 
 let level = 4
@@ -67,7 +69,9 @@ let assert_applicability err f st m x u w v =
       | _                                      -> assert false (**)
 
 let rec b_type_of err f st m z =
-   if !G.ct >= level then log1 st "Now checking" m z;
+IFDEF TRACE THEN
+   if !G.ct >= level then log1 st "Now checking" m z
+ELSE () END;
    match z with
    | B.Sort k                        ->
       let k = H.apply k in f z (B.Sort k) 
@@ -130,3 +134,5 @@ let rec b_type_of err f st m z =
 (* Interface functions ******************************************************)
 
 and type_of err f st m t = b_type_of err f st m t
+
+END