Commit bd126535 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (array changes).

parent 1f96e762
......@@ -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-02-14.2.a3cea59c") | (= "dev") }
"coq-iris" { (= "dev.2020-02-23.0.40c0674a") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......
......@@ -2537,7 +2537,7 @@ Proof.
pose (i := ((back `min` sz) - S n)%nat).
assert ((back `min` sz)%nat - S n = i) as -> by by rewrite Nat2Z.inj_sub.
(* We can now load. *)
wp_apply (wp_load_offset _ _ _ar i _ (array_get slots deqs i) with "Hℓ_ar");
wp_apply (wp_load_offset _ _ _ar _ i _ (array_get slots deqs i) with "Hℓ_ar");
[ apply array_content_lookup; lia | iIntros "Hℓa" ].
(* If there was an initial contradiction, it is still here. *)
iAssert match cont with
......@@ -2728,7 +2728,7 @@ Proof.
* (* The CmpXchg failed, we continue looping. *)
assert (array_content sz slots deqs !! i = Some NONEV).
{ rewrite array_content_lookup; last by lia. by rewrite Hi. }
wp_apply (wp_cmpxchg_fail_offset _ _ _ _ _ (array_get slots deqs i) with "Hℓ_ar");
wp_apply (wp_cmpxchg_fail_offset _ _ _ _ _ _ (array_get slots deqs i) with "Hℓ_ar");
[ by rewrite Hi | by rewrite Hi | by right | iIntros "Hℓa" (rs' ->) "Hp"].
(* We can close the invariant. *)
iModIntro. iSplitR "AU Hback_snap Hi2_lower_bound".
......
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