diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index ff18e12dac2eaf43a8554f61988c610ed84623e8..08a4c4c4391ab4bc137f14e7801469f5215675fb 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -1,4 +1,3 @@
-From iris.algebra Require Export upred_tactics.
 From iris.heap_lang Require Export tactics derived.
 Import uPred.
 
diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 3f0fbc0151e9a3081a9b38dbfc0eb22fae948de8..ff5944225792146a045b8c4607efb0ef7ac45e6d 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -1,5 +1,5 @@
 From iris.proofmode Require Export classes.
-From iris.algebra Require Import upred_big_op gmap upred_tactics.
+From iris.algebra Require Import upred_big_op gmap.
 Import uPred.
 
 Section classes.
@@ -225,7 +225,7 @@ Global Instance frame_sep_l R P1 P2 Q Q' :
 Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
 Global Instance frame_sep_r R P1 P2 Q Q' :
   Frame R P2 Q → MakeSep P1 Q Q' → Frame R (P1 ★ P2) Q' | 10.
-Proof. rewrite /Frame /MakeSep => <- <-. solve_sep_entails. Qed.
+Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc (comm _ R) assoc. Qed.
 
 Class MakeAnd (P Q PQ : uPred M) := make_and : P ∧ Q ⊣⊢ PQ.
 Global Instance make_and_true_l P : MakeAnd True P P.