Skip to content
Snippets Groups Projects
Commit b4038b7b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent d1a2a68f
No related branches found
No related tags found
No related merge requests found
Pipeline #41959 failed
...@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries. ...@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
""" """
depends: [ depends: [
"coq-iris" { (= "dev.2021-02-10.0.7b4a04ce") | (= "dev") } "coq-iris" { (= "dev.2021-02-14.0.842fb394") | (= "dev") }
] ]
build: [make "-j%{jobs}%"] build: [make "-j%{jobs}%"]
......
...@@ -131,7 +131,7 @@ Section mguard. ...@@ -131,7 +131,7 @@ Section mguard.
Send ty Send (mutexguard α ty). Send ty Send (mutexguard α ty).
Proof. Proof.
iIntros (??? [|[[]|][]]) "H"; try done. simpl. iRevert "H". 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 repeat match goal with
| |- (ty_own _ _ _) (ty_own _ _ _) => by apply send_change_tid' | |- (ty_own _ _ _) (ty_own _ _ _) => by apply send_change_tid'
| |- _ => f_equiv | |- _ => f_equiv
......
...@@ -221,7 +221,7 @@ Section rwlock. ...@@ -221,7 +221,7 @@ Section rwlock.
Send ty Sync ty Sync (rwlock ty). Send ty Sync ty Sync (rwlock ty).
Proof. Proof.
move=>??????/=. do 2 apply bi.exist_mono=>?. apply bi.sep_mono_r. 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. by rewrite rwlock_inv_change_tid_own rwlock_inv_change_tid_shr.
Qed. Qed.
End rwlock. End rwlock.
......
...@@ -128,7 +128,7 @@ Section rwlockreadguard. ...@@ -128,7 +128,7 @@ Section rwlockreadguard.
Sync ty Send (rwlockreadguard α ty). Sync ty Send (rwlockreadguard α ty).
Proof. Proof.
iIntros (??? [|[[]|][]]) "H"; try done. simpl. iRevert "H". 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 repeat lazymatch goal with
| |- (ty_shr _ _ _ _) (ty_shr _ _ _ _) => by apply sync_change_tid' | |- (ty_shr _ _ _ _) (ty_shr _ _ _ _) => by apply sync_change_tid'
| |- (rwlock_inv _ _ _ _ _ _) _ => by apply rwlock_inv_change_tid_shr | |- (rwlock_inv _ _ _ _ _ _) _ => by apply rwlock_inv_change_tid_shr
......
...@@ -132,7 +132,7 @@ Section rwlockwriteguard. ...@@ -132,7 +132,7 @@ Section rwlockwriteguard.
Send ty Send (rwlockwriteguard α ty). Send ty Send (rwlockwriteguard α ty).
Proof. Proof.
iIntros (??? [|[[]|][]]) "H"; try done. simpl. iRevert "H". 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 repeat lazymatch goal with
| |- (ty_own _ _ _) (ty_own _ _ _) => by apply send_change_tid' | |- (ty_own _ _ _) (ty_own _ _ _) => by apply send_change_tid'
| |- (rwlock_inv _ _ _ _ _ _) _ => by apply rwlock_inv_change_tid_own | |- (rwlock_inv _ _ _ _ _ _) _ => by apply rwlock_inv_change_tid_own
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment