From b4038b7b1f76e7a0d788e87677ee3bc9c7f45a97 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Feb 2021 14:27:11 +0100
Subject: [PATCH] Bump Iris.
---
coq-lambda-rust.opam | 2 +-
theories/typing/lib/mutex/mutexguard.v | 2 +-
theories/typing/lib/rwlock/rwlock.v | 2 +-
theories/typing/lib/rwlock/rwlockreadguard.v | 2 +-
theories/typing/lib/rwlock/rwlockwriteguard.v | 2 +-
5 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 6e7efb62..ba62ac1d 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
- "coq-iris" { (= "dev.2021-02-10.0.7b4a04ce") | (= "dev") }
+ "coq-iris" { (= "dev.2021-02-14.0.842fb394") | (= "dev") }
]
build: [make "-j%{jobs}%"]
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 11b48b8f..a8dca25c 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -131,7 +131,7 @@ Section mguard.
Send ty → Send (mutexguard α ty).
Proof.
iIntros (??? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
- iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+ iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_entails.
repeat match goal with
| |- (ty_own _ _ _) ≡ (ty_own _ _ _) => by apply send_change_tid'
| |- _ => f_equiv
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index b5f64b88..b4923b11 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -221,7 +221,7 @@ Section rwlock.
Send ty → Sync ty → Sync (rwlock ty).
Proof.
move=>??????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r.
- apply bi.equiv_spec. f_equiv.
+ apply bi.equiv_entails. f_equiv.
by rewrite rwlock_inv_change_tid_own rwlock_inv_change_tid_shr.
Qed.
End rwlock.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 55ffb196..f3d6ac78 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -128,7 +128,7 @@ Section rwlockreadguard.
Sync ty → Send (rwlockreadguard α ty).
Proof.
iIntros (??? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
- iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+ iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_entails.
repeat lazymatch goal with
| |- (ty_shr _ _ _ _) ≡ (ty_shr _ _ _ _) => by apply sync_change_tid'
| |- (rwlock_inv _ _ _ _ _ _) ≡ _ => by apply rwlock_inv_change_tid_shr
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 651ff4df..8b5666b3 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -132,7 +132,7 @@ Section rwlockwriteguard.
Send ty → Send (rwlockwriteguard α ty).
Proof.
iIntros (??? [|[[]|][]]) "H"; try done. simpl. iRevert "H".
- iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_spec.
+ iApply bi.exist_mono. iIntros (κ); simpl. apply bi.equiv_entails.
repeat lazymatch goal with
| |- (ty_own _ _ _) ≡ (ty_own _ _ _) => by apply send_change_tid'
| |- (rwlock_inv _ _ _ _ _ _) ≡ _ => by apply rwlock_inv_change_tid_own
--
GitLab