- we add the missing layer constraint on applicability condition

[helm.git] / helm / software / helena / src / basic_ag / bagType.ml

diff --git a/helm/software/helena/src/basic_ag/bagType.ml b/helm/software/helena/src/basic_ag/bagType.ml
index e76399c5fd9fa32eed829f2009587cc8181a7efc..b6f3deb558624b69369345836b0cf539542c2169 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagType.ml
+++ b/helm/software/helena/src/basic_ag/bagType.ml
@@ -23,11 +23,11 @@ module ZR = BagReduction
 
 (* Internal functions *******************************************************)
 
-let level = 3
+let level = 4
 
 let log1 st s c t =
    let s1, s2 = s ^ " in the envireonment", "the term" in
-   L.log st ZO.specs level (L.et_items1 s1 c s2 t)
+   L.log st ZO.specs (pred level) (L.et_items1 s1 c s2 t)
 
 let error1 err st c t =
    let sc = "In the envireonment" in
@@ -93,7 +93,7 @@ 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.trace > level then L.log st ZO.specs (succ level) (L.t_items1 "Just scanned" c w);
+           if !G.trace > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w);
            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)