diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index b85789b5a4ea5e2ff7cf88cc899df793f6e0993d..9d5f84d7fca628a905617733f9271e6ece09ce57 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -39,7 +39,7 @@ Section proofs.
   Proof. rewrite /cinv; apply _. Qed.
 
   Global Instance cinv_own_fractionnal γ : Fractional (cinv_own γ).
-  Proof. intros ??. by rewrite -own_op. Qed.
+  Proof. intros ??. by rewrite /cinv_own -own_op. Qed.
   Global Instance cinv_own_as_fractionnal γ q :
     AsFractional (cinv_own γ q) (cinv_own γ) q.
   Proof. split. done. apply _. Qed.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index c851970e96a273033000b91f32e1742c501069e8..a0ac009cfc75ea1a0a633e1edb8b2608217a1a62 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -87,7 +87,7 @@ Section gen_heap.
   Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
   Global Instance mapsto_fractional l v : Fractional (λ q, l ↦{q} v)%I.
   Proof.
-    intros p q. by rewrite mapsto_eq -own_op -auth_frag_op
+    intros p q. by rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op
       op_singleton pair_op agree_idemp.
   Qed.
   Global Instance mapsto_as_fractional l q v :
@@ -97,7 +97,7 @@ Section gen_heap.
   Lemma mapsto_agree l q1 q2 v1 v2 : l ↦{q1} v1 -∗ l ↦{q2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
     apply wand_intro_r.
-    rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
+    rewrite mapsto_eq /mapsto_def -own_op -auth_frag_op own_valid discrete_valid.
     f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
     by intros [_ ?%agree_op_invL'].
   Qed.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 6bc0bda63c99e56354a798a5b12b48702717cb4c..4ab1fd0292e1a33ace0493e7e49f329f32a06329 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -37,7 +37,8 @@ Section saved_prop.
     saved_prop_own γ x -∗ saved_prop_own γ y -∗ ▷ (x ≡ y).
   Proof.
     apply wand_intro_r.
-    rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
+    rewrite /saved_prop_own -own_op own_valid agree_validI agree_equivI.
+    rewrite later_equivI.
     set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
     set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
     assert (∀ z, G2 (G1 z) ≡ z) as help.