Commit 7068d035 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 8fde0c22
......@@ -9,7 +9,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/FP/iris-examples.git"
synopsis: "A collection of case studies for Iris"
depends: [
"coq-iris" { (= "dev.2020-04-02.0.4f6d4de7") | (= "dev") }
"coq-iris" { (= "dev.2020-04-02.5.fa438702") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......
......@@ -59,12 +59,13 @@ Proof.
iAssert ( (x x'))%I as "Hxx".
{ iCombine "Hγ" "Hγ'" as "Hγ2". iClear "Hγ Hγ'".
rewrite own_valid csum_validI /= agree_validI agree_equivI bi.later_equivI /=.
rewrite -{2}[x]oFunctor_id -{2}[x']oFunctor_id.
assert (HF : oFunctor_map F (cid, cid) oFunctor_map F (iProp_fold (Σ:=Σ) iProp_unfold, iProp_fold (Σ:=Σ) iProp_unfold)).
rewrite -{2}[x]oFunctor_map_id -{2}[x']oFunctor_map_id.
assert (HF : oFunctor_map F (cid, cid) oFunctor_map F (iProp_fold (Σ:=Σ)
iProp_unfold, iProp_fold (Σ:=Σ) iProp_unfold)).
{ apply ne_proper; first by apply _.
by split; intro; simpl; symmetry; apply iProp_fold_unfold. }
rewrite (HF x). rewrite (HF x').
rewrite !oFunctor_compose. iNext. by iRewrite "Hγ2". }
rewrite !oFunctor_map_compose. iNext. by iRewrite "Hγ2". }
iNext. iRewrite -"Hxx" in "Hx'".
iExists x; iFrame "Hγ". iApply (Ψ_join with "Hx Hx'").
Qed.
......
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