Commit 94000f59 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 3dc517e3
Pipeline #26409 failed with stage
in 15 minutes and 45 seconds
......@@ -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.2020-04-02.5.fa438702") | (= "dev") }
"coq-iris" { (= "dev.2020-04-04.2.c2367a65") | (= "dev") }
]
......@@ -121,7 +121,6 @@ Section flock.
Context `{heapG Σ, flockG Σ}.
Variable N : namespace.
Definition invN := N.@"flock_inv".
Definition lockN := N.@"flock_lock".
Definition resN := N.@"flock_res".
(** * Definitions **)
......@@ -217,7 +216,7 @@ Section flock.
Definition is_flock (γ : flock_name) (lk : val) : iProp Σ :=
(inv invN (flock_inv γ)
is_lock lockN (flock_lock_name γ) lk
is_lock (flock_lock_name γ) lk
(own (flock_state_name γ) (E Unlocked)))%I.
(** * Lemmata **)
......@@ -251,7 +250,7 @@ Section flock.
Lemma to_props_map_singleton_included fp q ρ:
{[ρ := q]} to_props_map fp fp !! ρ = Some ().
Proof.
rewrite singleton_included=> -[[q' av] []].
rewrite singleton_included_l=> -[[q' av] []].
rewrite /to_props_map lookup_fmap fmap_Some_equiv.
move=> -[[] [Hρ _]]//.
Qed.
......@@ -474,7 +473,7 @@ Section flock.
{ by apply auth_auth_valid. }
iMod (own_alloc (E E )) as (γ_ac_props) "[Hacprops1 Hacprops2]".
{ by apply excl_auth_valid. }
iApply (newlock_spec lockN (own γ_state (E Unlocked)) with "Hfrag").
iApply (newlock_spec (own γ_state (E Unlocked)) with "Hfrag").
iNext. iIntros (lk γ_lock) "#Hlock".
pose (γ := (Build_flock_name γ_lock γ_state γ_props γ_ac_props)).
iMod (inv_alloc invN _ (flock_inv γ) with "[-HΦ]") as "#Hinv".
......
......@@ -368,7 +368,7 @@ Section properties.
{[cl := (q, lv, to_agree v)]} to_locking_heap σ
lv', lv lv' σ !! cl = Some (lv', v).
Proof.
rewrite singleton_included=> -[[[q' lv'] av] []].
rewrite singleton_included_l=> -[[[q' lv'] av] []].
rewrite /to_gen_heap lookup_fmap fmap_Some_equiv => -[[lv'' av'] [Hl [/= -> ->]]].
move=> /Some_pair_included_total_2 [/Some_pair_included_total_2] [_] Hxb'.
move=> /to_agree_included /leibniz_equiv_iff=> ->. by exists lv''.
......@@ -378,7 +378,7 @@ Section properties.
{[l := to_agree (k,n)]} to_heap_block_info τ
b, τ !! l = Some b heap_block_info b = (k,n).
Proof.
rewrite singleton_included=> -[mn].
rewrite singleton_included_l=> -[mn].
rewrite /to_heap_block_info lookup_fmap fmap_Some_equiv=> -[[b [-> ->]]] /=.
move=> /Some_included_total /to_agree_included /leibniz_equiv_iff; eauto.
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