- we add the missing layer constraint on applicability condition

[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 2dfb2552dc375649f8c8e0f3fc6ebb7a82a021d8..fd06282fe886f5e922350fef0f87d56201bb5cc7 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -24,14 +24,14 @@ module BR = BrgReduction
 
 (* Internal functions *******************************************************)
 
-let level = 3
+let level = 4
 
 let message1 st1 m t1 =
    L.et_items1 "In the environment" m st1 t1
 
 let log1 st s m t =
    let s =  s ^ " the term" in
-   L.log st BR.specs level (message1 s m t) 
+   L.log st BR.specs (pred level) (message1 s m t) 
 
 let error1 err s m t =
    err (message1 s m t)
@@ -59,7 +59,8 @@ let assert_applicability err f st m u w v =
    match BR.xwhd st m None u with 
       | _, B.Sort _                      ->
          error1 err "not a function type" m u
-      | mu, B.Bind (_, B.Abst (_, u), _) -> 
+      | mu, B.Bind (_, B.Abst (n, u), _) -> 
+         if !G.cc && not (N.assert_not_zero st n) then error1 err "not a function type" m u else 
          if BR.are_convertible st mu zero u m zero w then f () else
         error3 err m v w ~mu u
       | _                                -> assert false (**)