- the disambiguation of unified binders continues

[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 c83c5e87f12fa4602b18f46541479e5120280ff7..e6704d0a967e52648d43fabdba92bbd148044fc4 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgValidity.ml
+++ b/helm/software/helena/src/basic_rg/brgValidity.ml
@@ -21,12 +21,14 @@ module BR = BrgReduction
 
 let level = 3
 
+let warn s = L.warn level s
+
 let message1 st1 m t1 =
    L.et_items1 "In the environment" m st1 t1
 
-let log1 s m t =
+let log1 st s m t =
    let s =  s ^ " the term" in
-   L.log BR.specs level (message1 s m t) 
+   L.log st BR.specs level (message1 s m t) 
 
 let error1 err s m t =
    err (message1 s m t)
@@ -44,20 +46,23 @@ let zero = Some 0
 let one = Some 1
 
 let assert_convertibility err f st m u t =
+   if !G.trace >= level then warn "Asserting convertibility for cast";
    if BR.are_convertible st m zero u m one t then f () else
    error2 err m u m t
 
 let assert_applicability err f st m v t =
+   if !G.trace >= level then warn "Asserting applicability";
    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
       | _                                -> assert false (**)
 
 let rec b_validate err f st m x =
-   if !G.trace >= level then log1 "Now checking" m x;
+   if !G.trace >= level then log1 st.S.lenv "Now checking" m x;
    match x with
    | B.Sort _         -> f ()
    | B.LRef (_, i)    ->