From e4a2ae490b3d5097396a84be27d8c090fae33aa4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 1 Mar 2016 19:30:09 +0100
Subject: [PATCH] fix name of recv_strengthen to recv_weaken

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

diff --git a/barrier/proof.v b/barrier/proof.v
index ca58bd09a..bdfd6f256 100644
--- a/barrier/proof.v
+++ b/barrier/proof.v
@@ -325,7 +325,7 @@ Proof.
       rewrite !wand_diag -!later_intro. solve_sep_entails.
 Qed.
 
-Lemma recv_strengthen l P1 P2 :
+Lemma recv_weaken l P1 P2 :
   (P1 -★ P2) ⊑ (recv l P1 -★ recv l P2).
 Proof.
   apply wand_intro_l. rewrite /recv. rewrite sep_exist_r. apply exist_mono=>γ.
@@ -339,7 +339,7 @@ Qed.
 Lemma recv_mono l P1 P2 :
   P1 ⊑ P2 → recv l P1 ⊑ recv l P2.
 Proof.
-  intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_strengthen.
+  intros HP%entails_wand. apply wand_entails. rewrite HP. apply recv_weaken.
 Qed.
 
 End proof.
-- 
GitLab