From fa9b9d1bdfed4a8c933e78a6dd749b6b39251009 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Feb 2016 14:06:41 +0100
Subject: [PATCH] fix viewshifts.v

---
 program_logic/viewshifts.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 0db7e6673..f473fe761 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -87,7 +87,7 @@ Qed.
 Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → P >{E}> Q ⊑ P >{E ∪ Ef}> Q.
 Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
 Lemma vs_open i P : ownI i P >{{[i]},∅}> ▷ P.
-Proof. intros; apply vs_alt, pvs_open. Qed.
+Proof. intros; apply vs_alt, pvs_openI. Qed.
 
 Lemma vs_open' E i P : i ∉ E → ownI i P >{{[i]} ∪ E,E}> ▷ P.
 Proof.
@@ -96,7 +96,7 @@ Proof.
 Qed.
 
 Lemma vs_close i P : (ownI i P ∧ ▷ P) >{∅,{[i]}}> True.
-Proof. intros; apply vs_alt, pvs_close. Qed.
+Proof. intros; apply vs_alt, pvs_closeI. Qed.
 
 Lemma vs_close' E i P : i ∉ E → (ownI i P ∧ ▷ P) >{E,{[i]} ∪ E}> True.
 Proof.
@@ -116,6 +116,6 @@ Proof. by intros; apply vs_alt, pvs_ownG_updateP_empty. Qed.
 Lemma vs_update E m m' : m ~~> m' → ownG m >{E}> ownG m'.
 Proof. by intros; apply vs_alt, pvs_ownG_update. Qed.
 Lemma vs_alloc E P : ¬set_finite E → ▷ P >{E}> (∃ i, ■ (i ∈ E) ∧ ownI i P).
-Proof. by intros; apply vs_alt, pvs_alloc. Qed.
+Proof. by intros; apply vs_alt, pvs_allocI. Qed.
 
 End vs.
-- 
GitLab