- we add the missing layer constraint on applicability condition

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

diff --git a/helm/software/helena/src/basic_ag/bagReduction.ml b/helm/software/helena/src/basic_ag/bagReduction.ml
index c9cc85e9b391d6c8edfcde60353da9c6e9fd6933..6524dda862961b0cabb5d504741237da9bb75787 100644 (file)
--- a/helm/software/helena/src/basic_ag/bagReduction.ml
+++ b/helm/software/helena/src/basic_ag/bagReduction.ml
@@ -38,7 +38,7 @@ type ho_whd_result =
 
 (* Internal functions *******************************************************)
 
-let level = 4
+let level = 5
 
 let term_of_whdr = function
    | Sort_ h              -> Z.Sort h
@@ -48,11 +48,11 @@ let term_of_whdr = function
 
 let log1 st s c t =
    let s1, s2 = s ^ " in the environment", "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 log2 st s cu u ct t =
    let s1, s2, s3 = s ^ " in the environment", "the term", "and in the environment" in
-   L.log st ZO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
+   L.log st ZO.specs (pred level) (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
 
 let empty_machine = {i = 0; c = Z.empty_lenv; s = []}