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

Bump Iris (`iPoseProof` changes).

parent f6a53721
No related branches found
No related tags found
No related merge requests found
Pipeline #21844 passed
Stage: build
    Hide whitespace changes
    Inline Side-by-side
    opam
    + 1
    − 1
    View file @ 045c8203
    ...@@ -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/reloc"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
    depends: [ depends: [
    "coq-iris" { (= "dev.2019-11-07.1.891124d6") | (= "dev") } "coq-iris" { (= "dev.2019-11-21.0.e0d10c05") | (= "dev") }
    "coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
    ] ]
    theories/experimental/helping/helping_stack.v
    + 1
    − 1
    View file @ 045c8203
    ...@@ -613,7 +613,7 @@ Section refinement. ...@@ -613,7 +613,7 @@ Section refinement.
    rel_alloc_l st as "Hst". rel_pure_l. rel_pure_l. rel_pure_l. rel_pure_l. rel_alloc_l st as "Hst". rel_pure_l. rel_pure_l. rel_pure_l. rel_pure_l.
    iMod (own_alloc (● to_offer_reg ∅ : authR offerRegR)) as (γo) "Hor". iMod (own_alloc (● to_offer_reg ∅ : authR offerRegR)) as (γo) "Hor".
    { apply auth_auth_valid. apply to_offer_reg_valid. } { apply auth_auth_valid. apply to_offer_reg_valid. }
    iMod (inv_alloc stackN _ (stackInv _ γo st st' mb lk) with "[-]") as "#Hinv". iMod (inv_alloc stackN _ (stackInv A γo st st' mb lk) with "[-]") as "#Hinv".
    { iNext. unfold stackInv. { iNext. unfold stackInv.
    iExists None, _, _. iFrame. iExists None, _, _. iFrame.
    iSplit; eauto. iSplit; eauto.
    ......
    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