let h xv vv xt tt cc = function
| R.Sort _ -> error1 "not a function" c xt
| R.Abst w ->
- L.box ();
+ L.box (succ level);
L.log O.specs (succ level) (L.ct_items1 "Just scanned" cc w);
- L.unbox ();
+ L.unbox (succ level);
let f b =
if b then f (S.sh2 v xv t xt x B.appl) (B.appl xv tt) else
error2 "the term" cc xv "must be of type" cc w
type_of f g c u
and type_of f g c x =
- let f t u = L.unbox (); f t u in
- L.box (); b_type_of f g c x
+ let f t u = L.unbox level; f t u in
+ L.box level; b_type_of f g c x