assign active memory in equivs

Author: oskgo

src/ecEnv.ml

@@ -1753,9 +1753,9 @@ module Fun = struct
     (pre1,pre2), (post1,post2)
 
   let equivF ml mr path1 path2 env =
-    let (pre1,pre2),(post1,post2) = equivF_memenv ml mr path1 path2 env in
-    Memory.push_all [pre1; pre2] env,
-    Memory.push_all [post1; post2] env
+    let (prel,prer),(postl,postr) = equivF_memenv ml mr path1 path2 env in
+    Memory.push_active_ts prel prer env,
+    Memory.push_active_ts postl postr env
 
   let equivS path1 path2 env =
     let fun1 = by_xpath path1 env in

src/ecTyping.ml

@@ -3030,7 +3030,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =
                         let trans1 (x, s) =
                           let mem =
                             match s with
-                            | None -> odfl mhr (EcEnv.Memory.get_active_ss env)
+                            | None -> oget (EcEnv.Memory.get_active_ss env)
                             | Some s -> transmem env s
 
                           in (transpvar env mem x, mem) in
@@ -3171,8 +3171,9 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =
 
          let do1 = function
           | GVvar x ->
-              let x1 = lookup EcFol.mleft  (qual (om |> omap fst) x) in
-              let x2 = lookup EcFol.mright (qual (om |> omap snd) x) in
+              let ml, mr = oget (EcEnv.Memory.get_active_ts env) in
+              let x1 = lookup ml (qual (om |> omap fst) x) in
+              let x2 = lookup mr (qual (om |> omap snd) x) in
                 unify_or_fail env ue x.pl_loc ~expct:x1.f_ty x2.f_ty;
                 f_eq x1 x2