- improved logging

[helm.git] / helm / software / lambda-delta / basic_ag / bagReduction.ml

diff --git a/helm/software/lambda-delta/basic_ag/bagReduction.ml b/helm/software/lambda-delta/basic_ag/bagReduction.ml
index 0310e8d2833de378e435ae3ffcf80b998da5dcad..b0cd88d6cc3b66d41136ec36fae68d2878f1270c 100644 (file)
--- a/helm/software/lambda-delta/basic_ag/bagReduction.ml
+++ b/helm/software/lambda-delta/basic_ag/bagReduction.ml
@@ -107,8 +107,8 @@ let rec ho_whd f c m x =
    whd aux c m x
    
 let ho_whd f c t =
-   let f c r = L.unbox (); f c r in
-   L.box (); L.log O.specs level (L.ct_items1 "Now scanning" c t);
+   let f c r = L.unbox level; f c r in
+   L.box level; L.log O.specs level (L.ct_items1 "Now scanning" c t);
    ho_whd f c empty_machine t
 
 let rec are_convertible f c m1 t1 m2 t2 =
@@ -148,7 +148,7 @@ and are_convertible_stacks f c m1 m2 =
    C.forall2 f map m1.s m2.s
 
 let are_convertible f c t1 t2 = 
-   let f b = L.unbox (); f b in
-   L.box ();
+   let f b = L.unbox level; f b in
+   L.box level;
    L.log O.specs level (L.ct_items2 "Now converting" c t1 "and" c t2);
    are_convertible f c empty_machine t1 empty_machine t2