X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgReduction.ml;h=03ed05b053a603985fea79550c313397b3cfe675;hb=da284829d696ab53dfa437e169fa669c8e58de7d;hp=5dff4647b43db3bd06f56153f146e443a4660dd8;hpb=ea41b1f6e212334924a8de4b2ff53b2586de9c4b;p=helm.git

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 5dff4647b..03ed05b05 100644
--- a/helm/software/lambda-delta/basic_rg/brgReduction.ml
+++ b/helm/software/lambda-delta/basic_rg/brgReduction.ml
@@ -170,7 +170,7 @@ and ac st m1 t1 m2 t2 =
 
 and ac_stacks st m1 m2 =
 (*   L.warn "entering R.are_convertible_stacks"; *)
-(*   if List.length m1.s <> List.length m2.s then false else *)
+   if List.length m1.s <> List.length m2.s then false else
    let map (c1, v1) (c2, v2) =
       let m1, m2 = {m1 with e = c1; s = []}, {m2 with e = c2; s = []} in
       ac {st with Y.si = false} m1 v1 m2 v2
@@ -194,7 +194,7 @@ let xwhd st m t =
 
 let are_convertible st mu u mw w = 
    L.box level; log2 "Now converting" mu.e u mw.e w;
-   let r = ac {st with Y.delta = false; Y.rt = false} mu u mw w in   
+   let r = ac {st with Y.delta = st.Y.expand; Y.rt = false} mu u mw w in   
    L.unbox level; r
 (*    let err _ = in 
       if S.eq mu mw then are_alpha_convertible err f u w else err () *)