X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_ag%2FbagType.ml;h=52c485ae740426c3a178d03efd4438593905390a;hb=426005acf6fb05116de5bae20591eefe55a4df00;hp=a651c6e3379b3dbf586009f3a1e28d9d828deef2;hpb=338e3e5c639fbcfeeb347a0121cacc6c0f1fc42a;p=helm.git

diff --git a/helm/software/lambda-delta/basic_ag/bagType.ml b/helm/software/lambda-delta/basic_ag/bagType.ml
index a651c6e33..52c485ae7 100644
--- a/helm/software/lambda-delta/basic_ag/bagType.ml
+++ b/helm/software/lambda-delta/basic_ag/bagType.ml
@@ -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