issues with res

Author: oskgo

src/ecTyping.ml

@@ -3199,12 +3199,13 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =
                   @ List.map (fun (xp, ty) -> f_pvar (EcTypes.pv_glob xp) ty mem) pv in
 
                 map_ss_inv f_tuple res in
-
-              let x1 = create EcFol.mleft  in
-              let x2 = create EcFol.mright in
+                  
+              let ml, mr = oget (EcEnv.Memory.get_active_ts env) in
+              let x1 = ss_inv_generalize_right (create ml) mr in
+              let x2 = ss_inv_generalize_left (create mr) ml in
 
               unify_or_fail env ue gp.pl_loc ~expct:x1.inv.f_ty x2.inv.f_ty;
-              (map_ss_inv2 f_eq x1 x2).inv
+              (map_ts_inv2 f_eq x1 x2).inv
         in
           EcFol.f_ands (List.map do1 xs)
 

src/phl/ecPhlCall.ml

@@ -368,17 +368,18 @@ let t_call side ax tc =
 
 (* -------------------------------------------------------------------- *)
 let mk_inv_spec (_pf : proofenv) env inv fl fr =
+  let ml, mr = inv.ml, inv.mr in
   match NormMp.is_abstract_fun fl env with
   | true ->
     let (topl, _, _, sigl),
       (topr, _, _  , sigr) = EcLowPhlGoal.abstract_info2 env fl fr in
-    let eqglob = ts_inv_eqglob topl mleft topr mright in
+    let eqglob = ts_inv_eqglob topl ml topr mr in
     let lpre = [eqglob;inv] in
     let eq_params =
       ts_inv_eqparams
-        sigl.fs_arg sigl.fs_anames mleft
-        sigr.fs_arg sigr.fs_anames mright in
-    let eq_res = ts_inv_eqres sigl.fs_ret mleft sigr.fs_ret mright in
+        sigl.fs_arg sigl.fs_anames ml
+        sigr.fs_arg sigr.fs_anames mr in
+    let eq_res = ts_inv_eqres sigl.fs_ret ml sigr.fs_ret mr in
     let pre    = map_ts_inv f_ands (eq_params::lpre) in
     let post   = map_ts_inv f_ands [eq_res; eqglob; inv] in
       f_equivF pre fl fr post
@@ -395,9 +396,9 @@ let mk_inv_spec (_pf : proofenv) env inv fl fr =
       if not testty then raise EqObsInError;
       let eq_params =
         ts_inv_eqparams
-          sigl.fs_arg sigl.fs_anames mleft
-          sigr.fs_arg sigr.fs_anames mright in
-      let eq_res = ts_inv_eqres sigl.fs_ret mleft sigr.fs_ret mright in
+          sigl.fs_arg sigl.fs_anames ml
+          sigr.fs_arg sigr.fs_anames mr in
+      let eq_res = ts_inv_eqres sigl.fs_ret ml sigr.fs_ret mr in
       let pre = map_ts_inv2 f_and eq_params inv in
       let post = map_ts_inv2 f_and eq_res inv in
         f_equivF pre fl fr post

src/phl/ecPhlConseq.ml

@@ -1405,7 +1405,7 @@ let process_conseq notmod ((info1, info2, info3) : conseq_ppterm option tuple3)
         in (penv, qenv, Inv_ts (ef_pr ef), Inv_ts (ef_po ef), tbool, lift_ts_inv2 fmake)
 
       | FequivS es ->
-        let env = LDecl.push_all [es.es_ml; es.es_mr] hyps in
+        let env = LDecl.push_active_ts es.es_ml es.es_mr hyps in
         let fmake pre post c_or_bd =
           ensure_none c_or_bd;
           f_equivS (snd es.es_ml) (snd es.es_mr) pre es.es_sl es.es_sr post