Commit 2da665c5 authored by Ralf Jung's avatar Ralf Jung

update dependencies; fix for agree_op rename

parent 36657093
Pipeline #34137 failed with stage
in 35 minutes and 54 seconds
......@@ -14,7 +14,7 @@ the type system, and safety proof for some Rust libraries.
"""
depends: [
"coq-iris" { (= "dev.2020-09-03.1.7dd1b9af") | (= "dev") }
"coq-iris" { (= "dev.2020-09-15.1.5a2a5bec") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -143,7 +143,7 @@ Section heap.
Proof.
rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
eapply pure_elim; [done|]=> /auth_frag_valid /=.
rewrite singleton_op -pair_op singleton_valid=> -[? /agree_op_invL'->]; eauto.
rewrite singleton_op -pair_op singleton_valid=> -[? /to_agree_op_inv_L->]; eauto.
Qed.
Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] True.
......
......@@ -66,7 +66,7 @@ Proof.
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move : Hγs.
rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /agree_op_invL' <-.
rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L <-.
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
Global Instance own_bor_into_op κ x x1 x2 :
......@@ -100,7 +100,7 @@ Proof.
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move: Hγs.
rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /agree_op_invL'=> <-.
rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L=> <-.
iExists γs. iSplit; first done. rewrite own_op; iFrame.
Qed.
Global Instance own_cnt_into_op κ x x1 x2 :
......@@ -134,7 +134,7 @@ Proof.
iIntros "[Hx Hy]".
iDestruct "Hx" as (γs) "[Hγs Hx]"; iDestruct "Hy" as (γs') "[Hγs' Hy]".
iDestruct (own_valid_2 with "Hγs Hγs'") as %Hγs. move: Hγs.
rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /agree_op_invL'=> <-.
rewrite -auth_frag_op auth_frag_valid singleton_op singleton_valid=> /to_agree_op_inv_L=> <-.
iExists γs. iSplit. done. rewrite own_op; iFrame.
Qed.
Global Instance own_inh_into_op κ x x1 x2 :
......
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