Skip to content

I
Iron
Commit 8aacd098 authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

bump Iris

parent e09691b5
Pipeline #17686 passed with stage
    in 15 minutes and 18 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 3 additions and 3 deletions
    opam
    View file @ 8aacd098
    ......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
    install: [make "install"]
    remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
    depends: [
    "coq-iris" { (= "dev.2019-06-12.3.1a0c5860") | (= "dev") }
    "coq-iris" { (= "dev.2019-06-13.0.860bd8e4") | (= "dev") }
    ]
    theories/iron_logic/adequacy.v
    View file @ 8aacd098
    ......@@ -44,7 +44,7 @@ Proof.
    intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
    eapply (wp_strong_adequacy Σ _); [|done]=> ?.
    iMod Hwp as (perm stateI fork_post ?? P) "(Hσ&Hp&Hwp)". clear Hwp.
    iExists stateI, _, fork_post. iIntros "!> {$Hσ}".
    iExists s, stateI, _, fork_post. iIntros "!> {$Hσ}".
    rewrite iron_wp_eq /=. iSplitL. iApply ("Hwp" with "Hp").
    iIntros (e2 t2' -> Hsafe) "Hσ Hpost _". rewrite bi.pure_and; iFrame (Hsafe).
    iIntros (v t2'' [= -> <-]). rewrite to_of_val /=.
    ......@@ -83,7 +83,7 @@ Proof.
    intros Hwp [n [κs Hsteps]]%erased_steps_nsteps.
    eapply (wp_strong_adequacy Σ _); [|done]=> ?.
    iMod Hwp as (perm stateI fork_post ?? P) "(Hσ&Hp&Hwp)".
    iExists stateI, _, fork_post. iIntros "!> {$Hσ}"; csimpl.
    iExists s, stateI, _, fork_post. iIntros "!> {$Hσ}"; csimpl.
    rewrite iron_wp_eq /=. iSplitL. iApply ("Hwp" with "Hp").
    iIntros (?? [= <- <-] _) "Hσ". rewrite fmap_length to_of_val Hmap_val.
    iDestruct 1 as (π1 π2' ->) "[Hp H]". rewrite fracPred_at_sep.
    ......
    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