the sort hierarchy parameter enter the kernel status

[helm.git] / helm / software / lambda-delta / basic_rg / brgReduction.ml

diff --git a/helm/software/lambda-delta/basic_rg/brgReduction.ml b/helm/software/lambda-delta/basic_rg/brgReduction.ml
index 5dff4647b43db3bd06f56153f146e443a4660dd8..03ed05b053a603985fea79550c313397b3cfe675 100644 (file)
--- 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 () *)