From 17522e1cb6b91cee895792faedb7c80046701d5c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Nov 2017 17:27:31 +0100
Subject: [PATCH] Show that `saved_anything` is non-expansive and proper.

---
 theories/base_logic/lib/saved_prop.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index d7c76c2a5..5ba19e758 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -32,6 +32,11 @@ Section saved_anything.
     Persistent (saved_anything_own γ x).
   Proof. rewrite /saved_anything_own; apply _. Qed.
 
+  Global Instance saved_anything_ne γ : NonExpansive (saved_anything_own γ).
+  Proof. solve_proper. Qed.
+  Global Instance saved_anything_proper γ : Proper ((≡) ==> (≡)) (saved_anything_own γ).
+  Proof. solve_proper. Qed.
+
   Lemma saved_anything_alloc_strong x (G : gset gname) :
     (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_anything_own γ x)%I.
   Proof. by apply own_alloc_strong. Qed.
-- 
GitLab