From c938bc452c30a2d8f13af1304d38081afe4399e2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Feb 2016 11:43:12 +0100
Subject: [PATCH] Rename saved_prop_twice -> saved_prop_agree.

---
 program_logic/saved_prop.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/program_logic/saved_prop.v b/program_logic/saved_prop.v
index d8b072b05..96c2b8367 100644
--- a/program_logic/saved_prop.v
+++ b/program_logic/saved_prop.v
@@ -16,14 +16,14 @@ Section saved_prop.
   Implicit Types γ : gname.
 
   Lemma saved_prop_alloc_strong N P (G : gset gname) :
-    True ⊑ pvs N N (∃ γ, ■(γ ∉ G) ∧ saved_prop_own SPI γ P).
+    True ⊑ pvs N N (∃ γ, ■ (γ ∉ G) ∧ saved_prop_own SPI γ P).
   Proof. by apply own_alloc_strong. Qed.
 
   Lemma saved_prop_alloc N P :
     True ⊑ pvs N N (∃ γ, saved_prop_own SPI γ P).
   Proof. by apply own_alloc. Qed.
 
-  Lemma saved_prop_twice γ P Q :
+  Lemma saved_prop_agree γ P Q :
     (saved_prop_own SPI γ P ★ saved_prop_own SPI γ Q) ⊑ ▷ (P ↔ Q).
   Proof.
     rewrite /saved_prop_own -own_op own_valid agree_validI.
-- 
GitLab