diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 8c3bc73bdb49edadfe489c4aa202e64bc8c3cdc7..e6a3b0f624cf1d4716c526b42fb973b1a2ce0ff6 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -45,11 +45,17 @@ Implicit Types P Q : iProp Σ.
 
 Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
 Proof. solve_proper. Qed.
+Global Instance box_own_prop_contractive γ : Contractive (box_own_prop γ).
+Proof. solve_contractive. Qed.
+
 Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (slice_inv γ).
 Proof. solve_proper. Qed.
 
 Global Instance slice_ne n γ : Proper (dist n ==> dist n) (slice N γ).
 Proof. solve_proper. Qed.
+Global Instance slice_contractive γ : Contractive (slice N γ).
+Proof. solve_contractive. Qed.
+
 Global Instance slice_persistent γ P : PersistentP (slice N γ P).
 Proof. apply _. Qed.
 
diff --git a/theories/base_logic/lib/core.v b/theories/base_logic/lib/core.v
index fe6a0ed7de8cc79324f354c4961dcf746af17bda..ccabc7ecf33ebb83ee3474e82a1d30043c583615 100644
--- a/theories/base_logic/lib/core.v
+++ b/theories/base_logic/lib/core.v
@@ -37,4 +37,4 @@ Section core.
   Qed.
 End core.
 
-Global Opaque coreP.
\ No newline at end of file
+Global Opaque coreP.