Skip to content
Snippets Groups Projects
Commit 9843e3f0 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Bump Iris, fix build.

parent 42ccca26
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
opam
+ 1
− 1
View file @ 9843e3f0
...@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"] ...@@ -11,5 +11,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ] remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [ depends: [
"coq-iris" { (= "dev.2018-02-21.1") | (= "dev") } "coq-iris" { (= "dev.2018-02-23.0") | (= "dev") }
] ]
theories/lifetime/model/borrow.v
+ 1
− 1
View file @ 9843e3f0
...@@ -41,7 +41,7 @@ Proof. ...@@ -41,7 +41,7 @@ Proof.
rewrite /lft_bor_alive. iExists _. iFrame "HboxB HB●". rewrite /lft_bor_alive. iExists _. iFrame "HboxB HB●".
iApply @big_sepM_insert; first by destruct (B !! γB). iApply @big_sepM_insert; first by destruct (B !! γB).
simpl. iFrame. } simpl. iFrame. }
iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iExists _, _; iFrame|]. iMod ("Hclose" with "[HA HI Hclose']") as "_"; [by iNext; iExists _, _; iFrame|].
iSplitL "HB◯ HsliceB". iSplitL "HB◯ HsliceB".
+ rewrite /bor /raw_bor /idx_bor_own. iModIntro. iExists γB. iFrame. + rewrite /bor /raw_bor /idx_bor_own. iModIntro. iExists γB. iFrame.
iExists P. rewrite -uPred.iff_refl. auto. iExists P. rewrite -uPred.iff_refl. auto.
......
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