- we add the missing layer constraint on applicability condition

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

diff --git a/helm/software/helena/src/basic_rg/brgValidity.ml b/helm/software/helena/src/basic_rg/brgValidity.ml
index 458962b1f5aa69c31365a4dcb0b082afe10924eb..d028e058527d8bc08ecfd0aa9b94650e8941eebc 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -11,6 +11,7 @@
 
 module L  = Log
 module G  = Options
+module N  = Layer
 module E  = Entity
 module B  = Brg
 module BE = BrgEnvironment
@@ -18,16 +19,16 @@ module BR = BrgReduction
 
 (* Internal functions *******************************************************)
 
-let level = 3
+let level = 4
 
-let warn s = L.warn level s
+let warn s = L.warn (pred level) s
 
 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)
@@ -54,10 +55,13 @@ let assert_applicability err f st m v t =
    match BR.xwhd st m None t with 
       | _, B.Sort _                      ->
          error1 err "not a function" m t
-      | mw, B.Bind (_, B.Abst (_, w), _) ->
-         if !G.trace >= level then warn "Asserting convertibility for application";
-         if BR.are_convertible st mw zero w m one v then f () else
-        error2 err mw w m v
+      | mw, B.Bind (_, B.Abst (n, w), _) ->
+         if !G.cc && not (N.assert_not_zero st n) then error1 err "not a function" m t
+         else begin
+            if !G.trace >= level then warn "Asserting convertibility for application";
+            if BR.are_convertible st mw zero w m one v then f () else
+           error2 err mw w m v
+         end
       | _                                -> assert false (**)
 
 let rec b_validate err f st m x =