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

Bump Iris.

parent 93f148a6
No related branches found
No related tags found
No related merge requests found
Pipeline #14279 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
opam
+ 1
− 1
View file @ 99dbfb39
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [ depends: [
"coq-iris" { (= "dev.2019-01-25.3.6a8c782b") | (= "dev") } "coq-iris" { (= "dev.2019-01-27.0.9896799d") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
] ]
theories/hocap/shared_bag.v
+ 1
− 1
View file @ 99dbfb39
...@@ -55,7 +55,7 @@ Section proof. ...@@ -55,7 +55,7 @@ Section proof.
iMod (bag_contents_update b ({[v]} ∪ Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]". iMod (bag_contents_update b ({[v]} ∪ Y) with "[$Hb1 $Hb2]") as "[Hb1 Hb2]".
iFrame. iApply "Hcl". iFrame. iApply "Hcl".
iNext. iExists _; iFrame. iNext. iExists _; iFrame.
rewrite big_sepMS_union big_sepMS_singleton. iFrame. } rewrite big_sepMS_singleton. iFrame. }
{ iNext. iIntros "_". iApply "HΦ". by iFrame "Hinv". } { iNext. iIntros "_". iApply "HΦ". by iFrame "Hinv". }
Qed. Qed.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment