- we add the missing layer constraint on applicability condition

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

diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml
index 08f3a340756e8187297fa966e38e54e5394f1b36..e20737ec4c04fcc4147ece4c1dd195d6ffb9295d 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgReduction.ml
+++ b/helm/software/helena/src/basic_rg/brgReduction.ml
@@ -33,17 +33,17 @@ type message = (rtm, B.term) L.message
 
 (* Internal functions *******************************************************)
 
-let level = 4
+let level = 5
 
 let sublevel = succ level
 
 let log1 st s c t =
    let s1, s2 = s ^ " in the environment", "the term" in
-   L.log st BO.specs level (L.et_items1 s1 c s2 t)
+   L.log st BO.specs (pred level) (L.et_items1 s1 c s2 t)
 
 let log2 st s cu u ct t =
    let s1, s2, s3 = s ^ " in the environment (expected)", "the term", "and in the environment (inferred)" in
-   L.log st BO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+   L.log st BO.specs (pred level) (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
 
 let rec list_and map = function
    | hd1 :: tl1, hd2 :: tl2 ->