- the disambiguation of unified binders continues

[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 5ba07c876355a1e63e8ec3b4c1c6f93873b1285f..43e193edee22d2336000ce88580e94230ba83f39 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgType.ml
+++ b/helm/software/helena/src/basic_rg/brgType.ml
@@ -30,9 +30,9 @@ let level = 3
 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)
@@ -66,7 +66,7 @@ let assert_applicability err f st m u w v =
       | _                                -> assert false (**)
 
 let rec b_type_of 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 (a, h)           ->
       let h = H.apply h in f x (B.Sort (a, h)) 
@@ -101,7 +101,7 @@ let rec b_type_of err f st m x =
       type_of err f st m v
    | B.Bind (a, B.Abst (n, u), t) ->
       let f xu xt tt =
-        f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus n 1) a xu tt)
+        f (W.sh2 u xu t xt x (B.bind_abst n a)) (B.bind_abst (N.minus st.S.lenv n 1) a xu tt)
       in
       let f xu m = b_type_of err (f xu) st m t in
       let f xu _ = f xu (BR.push m a (B.abst n xu)) in