From dcab926cb7c2c21a7bedd647037ba49747cfe8fe Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 23 Dec 2016 18:06:19 +0100
Subject: [PATCH] Slices are contractive.

---
 theories/base_logic/lib/boxes.v | 6 ++++++
 theories/base_logic/lib/core.v  | 2 +-
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 8c3bc73bd..e6a3b0f62 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 fe6a0ed7d..ccabc7ecf 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.
-- 
GitLab