diff --git a/src/ecCoreFol.ml b/src/ecCoreFol.ml
index 8b6a39d020..9118a71c8a 100644
--- a/src/ecCoreFol.ml
+++ b/src/ecCoreFol.ml
@@ -1844,12 +1844,11 @@ module Fsubst = struct
 
     | FeHoareS hs ->
         assert (not (Mid.mem (fst hs.ehs_m) s.fs_mem));
-        let es  = e_subst_init s.fs_freshen s.fs_sty.ts_p
-                               s.fs_ty s.fs_opdef s.fs_sty.ts_mp s.fs_esloc in
+        let es  = e_subst_init s.fs_freshen s.fs_ty s.fs_esloc in
         let ehs_pr  = f_subst ~tx s hs.ehs_pr in
         let ehs_po  = f_subst ~tx s hs.ehs_po in
         let ehs_s  = EcCoreModules.s_subst es hs.ehs_s in
-        let ehs_m = EcMemory.me_subst s.fs_mem s.fs_ty hs.ehs_m in
+        let ehs_m = EcMemory.me_subst s.fs_mem (ty_subst s.fs_ty) hs.ehs_m in
         f_eHoareS ehs_m ehs_pr ehs_s ehs_po
 
     | FcHoareF chf ->
diff --git a/src/ecReduction.ml b/src/ecReduction.ml
index e8e19e7220..32db20fccd 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -259,7 +259,7 @@ end) = struct
   let add_modules env p1 p2 : EcEnv.env * EcSubst.subst =
     List.fold_left2 (fun (env, s) (id1,_) (id2,mt) ->
         let env = EcEnv.Mod.bind_local id2 mt env in
-        env, EcSubst.add_module s id1 (EcPath.mident id2)) EcSubst.empty p1 p2
+        env, EcSubst.add_module s id1 (EcPath.mident id2)) (env, EcSubst.empty) p1 p2
 
   (* ------------------------------------------------------------------ *)
   let rec for_module_type env ~norm mt1 mt2 =