let level = 3
-let log1 s c t =
- let sc, st = s ^ " in the envireonment", "the term" in
- L.log ZO.specs level (L.et_items1 sc c st t)
+let log1 st s c t =
+ let s1, s2 = s ^ " in the envireonment", "the term" in
+ L.log st ZO.specs level (L.et_items1 s1 c s2 t)
let error1 err st c t =
let sc = "In the envireonment" in
let rec b_type_of err f st c x =
(* L.warn "Entering T.b_type_of"; *)
- if !G.trace >= level then log1 "Now checking" c x;
+ if !G.trace >= level then log1 st.S.lenv "Now checking" c x;
match x with
| Z.Sort h ->
let h = H.apply h in f x (Z.Sort h)
| Z.Appl (v, t) ->
let f xv vv xt tt = function
| ZR.Abst w ->
- if !G.trace > level then L.log ZO.specs (succ level) (L.t_items1 "Just scanned" c w);
+ if !G.trace > level then L.log st.S.lenv ZO.specs (succ level) (L.t_items1 "Just scanned" c w);
let f a =
(* L.warn (Printf.sprintf "Convertible: %b" a); *)
if a then f (W.sh2 v xv t xt x Z.appl) (Z.appl xv tt)