]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_ag/bagType.ml
- improved logging
[helm.git] / helm / software / lambda-delta / basic_ag / bagType.ml
index a651c6e3379b3dbf586009f3a1e28d9d828deef2..52c485ae740426c3a178d03efd4438593905390a 100644 (file)
@@ -90,9 +90,9 @@ let rec b_type_of f g c x =
       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
@@ -117,5 +117,5 @@ let rec b_type_of f g c x =
       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