Commit 4dcc1427 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 5587b018
Pipeline #26407 failed with stage
in 16 minutes and 18 seconds
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [ depends: [
"coq-iris" { (= "dev.2020-03-27.1.6eb52a82") | (= "dev") } "coq-iris" { (= "dev.2020-04-04.3.9b2ad256") | (= "dev") }
] ]
...@@ -91,7 +91,7 @@ Section to_heap. ...@@ -91,7 +91,7 @@ Section to_heap.
Lemma heap_singleton_included σ l q v : Lemma heap_singleton_included σ l q v :
{[l := (q, to_agree v)]} to_heap σ σ !! l = Some v. {[l := (q, to_agree v)]} to_heap σ σ !! l = Some v.
Proof. Proof.
rewrite singleton_included=> -[[q' av] []]. rewrite singleton_included_l=> -[[q' av] []].
rewrite /to_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]]. rewrite /to_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //. move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
Qed. Qed.
...@@ -241,7 +241,7 @@ Section heap. ...@@ -241,7 +241,7 @@ Section heap.
iDestruct "HQs" as "[HQ HQs]". iDestruct "HQ" as (j π) "[Hp' Hj]". iDestruct "HQs" as "[HQ HQs]". iDestruct "HQ" as (j π) "[Hp' Hj]".
iAssert πfs !! j = Some π %I as %Hj. iAssert πfs !! j = Some π %I as %Hj.
{ iDestruct (own_valid_2 with "Hn Hj") { iDestruct (own_valid_2 with "Hn Hj")
as %[Hj%singleton_included Hvalid]%auth_both_valid. as %[Hj%singleton_included_l Hvalid]%auth_both_valid.
destruct Hj as (eπ'&Hj%leibniz_equiv&[[=]|(?&?&[= <-]&[= <-]&Heπ)]%option_included). destruct Hj as (eπ'&Hj%leibniz_equiv&[[=]|(?&?&[= <-]&[= <-]&Heπ)]%option_included).
destruct Heπ as [<-%leibniz_equiv|Hincl]; last first. destruct Heπ as [<-%leibniz_equiv|Hincl]; last first.
{ exfalso. move: (Hvalid j). rewrite Hj. destruct eπ'=> //. { exfalso. move: (Hvalid j). rewrite Hj. destruct eπ'=> //.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment