From 653b8d3facc3a3d08c0a68d0956f526cc6e2be54 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 10 Feb 2016 08:32:59 +0100
Subject: [PATCH] no reason for this prime

---
 program_logic/ghost_ownership.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index 421f05067..94bf6a0ea 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -69,7 +69,7 @@ Lemma own_valid γ a : own i γ a ⊑ ✓ a.
 Proof.
   rewrite /own ownG_valid; apply valid_mono=> ?; apply to_globalC_validN.
 Qed.
-Lemma own_valid_r' γ a : own i γ a ⊑ (own i γ a ★ ✓ a).
+Lemma own_valid_r γ a : own i γ a ⊑ (own i γ a ★ ✓ a).
 Proof. apply (uPred.always_entails_r' _ _), own_valid. Qed.
 Global Instance own_timeless γ a : Timeless a → TimelessP (own i γ a).
 Proof. unfold own; apply _. Qed.
-- 
GitLab