Skip to content

C
c
Commit 8caf5c0d authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Bump Iris. 

And revert some changes due to stdpp!80
parent 821b452a
Pipeline #18044 passed with stage
    in 16 minutes and 10 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 3 additions and 3 deletions
    opam
    View file @ 8caf5c0d
    ......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
    install: [make "install"]
    remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
    depends: [
    "coq-iris" { (= "dev.2019-06-26.0.ad3e5066") | (= "dev") }
    "coq-iris" { (= "dev.2019-06-26.1.4832f461") | (= "dev") }
    ]
    theories/lib/mset.v
    View file @ 8caf5c0d
    ......@@ -50,7 +50,7 @@ Section mset.
    iIntros (<- Hvc Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
    wp_lam; wp_pures. wp_load. wp_let.
    wp_apply (llist_member_spec with "[//]"). iIntros "_".
    rewrite (bool_decide_iff _ (v ∈ val_for_compare <$> vs)); last set_solver -Hvc.
    rewrite (bool_decide_iff _ (v ∈ val_for_compare <$> vs)); last set_solver.
    rewrite Hvc. iApply "HΦ". iExists l, hd, vs; auto.
    Qed.
    ......@@ -65,7 +65,7 @@ Section mset.
    iIntros (<- Hvc ? Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
    wp_lam. wp_pures. wp_load. wp_let. wp_apply wp_assert.
    wp_apply (llist_member_spec with "[//]"); iIntros "_".
    rewrite Hvc bool_decide_false /=; last set_solver -Hvc. wp_op; iSplit=> //; iIntros "!>".
    rewrite Hvc bool_decide_false /=; last set_solver. wp_op; iSplit=> //; iIntros "!>".
    wp_seq. wp_apply (lcons_spec with "[//]"); iIntros (hd' ?). wp_store.
    iApply "HΦ". iExists l, hd', (v :: vs). iFrame "Hl".
    rewrite NoDup_cons fmap_cons Hvc. assert (v ∉ vs).
    ......
    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