Commit 0a8f1911 authored by Ralf Jung's avatar Ralf Jung

update dependencies

parent 10d32e09
......@@ -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-07.0.86b62616") | (= "dev") }
"coq-iris" { (= "dev.2020-04-07.7.64bed0ca") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......
......@@ -169,7 +169,7 @@ Section gc.
Proof.
iIntros "Hgc_l". rewrite /gc_mapsto.
assert (Excl' v = (Excl' v) None)%I as ->. { done. }
rewrite -op_singleton auth_frag_op own_op.
rewrite -singleton_op auth_frag_op own_op.
iDestruct "Hgc_l" as "[_ H◯_none]".
iFrame.
Qed.
......
......@@ -24,7 +24,7 @@ Section Rules.
Lemma stack_mapstos_agree l v w : l ↦ˢᵗᵏ v l ↦ˢᵗᵏ w v = w.
Proof.
rewrite -own_op -auth_frag_op op_singleton own_valid.
rewrite -own_op -auth_frag_op singleton_op own_valid.
by iIntros (->%auth_frag_valid%singleton_valid%agree_op_invL').
Qed.
......
......@@ -140,7 +140,7 @@ Section cfg.
Proof.
apply wand_intro_r.
rewrite /heapS_mapsto -own_op -auth_frag_op own_valid discrete_valid.
f_equiv=> -[_] /=. rewrite op_singleton singleton_valid -pair_op.
f_equiv=> -[_] /=. rewrite singleton_op singleton_valid -pair_op.
by intros [_ ?%agree_op_invL'].
Qed.
Lemma mapstoS_combine l q1 q2 v1 v2 :
......
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