Skip to content
Snippets Groups Projects
Commit 77a0dd03 authored by Ralf Jung's avatar Ralf Jung
Browse files

update dependencies; fix for std++ lemma rename

parent aafa3afd
No related branches found
No related tags found
No related merge requests found
Pipeline #35511 passed
Hide whitespace changes
Inline Side-by-side
opam
+ 1
− 1
View file @ 77a0dd03
...@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries. ...@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
""" """
depends: [ depends: [
"coq-iris" { (= "dev.2020-10-01.3.8f6c063a") | (= "dev") } "coq-iris" { (= "dev.2020-10-02.0.5ab2529d") | (= "dev") }
] ]
build: [make "-j%{jobs}%"] build: [make "-j%{jobs}%"]
......
theories/lifetime/frac_borrow.v
+ 1
− 1
View file @ 77a0dd03
...@@ -76,7 +76,7 @@ Section frac_bor. ...@@ -76,7 +76,7 @@ Section frac_bor.
iIntros "#Hφ (H & Hown & Hφ1)". iNext. iIntros "#Hφ (H & Hown & Hφ1)". iNext.
iDestruct "H" as (qφ) "(Hφqφ & Hown' & [%|Hq])". iDestruct "H" as (qφ) "(Hφqφ & Hown' & [%|Hq])".
{ subst. iCombine "Hown'" "Hown" as "Hown". { subst. iCombine "Hown'" "Hown" as "Hown".
by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_q_ge_1. } by iDestruct (own_valid with "Hown") as %Hval%Qp_not_plus_ge. }
rewrite /frac_bor_inv. iApply bi.sep_exist_r. iExists (q + qφ)%Qp. rewrite /frac_bor_inv. iApply bi.sep_exist_r. iExists (q + qφ)%Qp.
iDestruct "Hq" as (q' Hqφq') "Hq'κ". iCombine "Hown'" "Hown" as "Hown". iDestruct "Hq" as (q' Hqφq') "Hq'κ". iCombine "Hown'" "Hown" as "Hown".
iDestruct (own_valid with "Hown") as %Hval. rewrite comm_L. iFrame "Hown". iDestruct (own_valid with "Hown") as %Hval. rewrite comm_L. iFrame "Hown".
......
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