X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_ag%2FbagType.ml;h=f92919ec791956ca4fa1e51f538994ef2ff8c4e4;hb=1b4d894e7349bba991823249f1716fb8f18239b7;hp=1f47b60ddc4a005fac7ebeaff5f5362abaa74c3a;hpb=fec20705af4705f8eb9542aece87769b82a6a6b4;p=helm.git diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml index 1f47b60dd..f92919ec7 100644 --- a/helm/software/helena/src/basic_ag/bagType.ml +++ b/helm/software/helena/src/basic_ag/bagType.ml @@ -21,6 +21,8 @@ module ZO = BagOutput module ZE = BagEnvironment module ZR = BagReduction +IFDEF TYPE THEN + (* Internal functions *******************************************************) let level = 4 @@ -45,7 +47,9 @@ let mk_gref u l = let rec b_type_of err f st c x = (* L.warn "Entering T.b_type_of"; *) - if !G.ct >= level then log1 st "Now checking" c x; +IFDEF TRACE THEN + if !G.ct >= level then log1 st "Now checking" c x +ELSE () END; match x with | Z.Sort h -> let h = H.apply h in f x (Z.Sort h) @@ -93,7 +97,9 @@ let rec b_type_of err f st c x = | Z.Appl (v, t) -> let f xv vv xt tt = function | ZR.Abst w -> - if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w); +IFDEF TRACE THEN + if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w) +ELSE () END; let f a = (* L.warn (Printf.sprintf "Convertible: %b" a); *) if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt) @@ -118,3 +124,5 @@ let rec b_type_of err f st c x = (* Interface functions ******************************************************) and type_of err f st c x = b_type_of err f st c x + +END