diff --git a/barrier/proof.v b/barrier/proof.v
index bb051fec74e34a7b7d6ca352c9448a049409f1f6..af6c271c15374c29d6f4e199ffd829ea2227ebc4 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.
diff --git a/barrier/specification.v b/barrier/specification.v
index 499e810e057089afb9c6bfd4d251919111f95075..f7a42b1f55da658f4c676d8fa3440f72473bad31 100644
--- a/barrier/specification.v
+++ b/barrier/specification.v
@@ -29,6 +29,6 @@ Proof.
   - intros l P. apply ht_alt.
     by rewrite -(wait_spec heapN N l P) wand_diag right_id.
   - intros l P Q. apply vs_alt. rewrite -(recv_split heapN N N l P Q) //.
-  - intros l P Q. apply recv_strengthen.
+  - intros l P Q. apply recv_weaken.
 Qed.
 End spec.