Commit b815eba9 authored by Ralf Jung's avatar Ralf Jung

update dependencies; fix for fmap_seq rename

parent a9043adb
......@@ -11,7 +11,7 @@ synopsis: "This is the Coq development of the Iris Project"
depends: [
"coq" { (>= "8.9.1" & < "8.12~") | (= "dev") }
"coq-stdpp" { (= "dev.2020-03-10.2.8db97649") | (= "dev") }
"coq-stdpp" { (= "dev.2020-03-17.3.ad2e80d6") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -91,7 +91,7 @@ Lemma mapsto_seq_array l q v n :
Proof.
rewrite /array. iInduction n as [|n'] "IH" forall (l); simpl.
{ done. }
iIntros "[$ Hl]". rewrite -fmap_seq big_sepL_fmap.
iIntros "[$ Hl]". rewrite -fmap_S_seq big_sepL_fmap.
setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
setoid_rewrite <-loc_add_assoc. iApply "IH". done.
Qed.
......
......@@ -249,7 +249,7 @@ Proof.
{ apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
intros (j&?&Hjl&_)%heap_array_lookup.
rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
rewrite loc_add_0 -fmap_seq big_sepL_fmap.
rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
setoid_rewrite <-loc_add_assoc.
rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
......@@ -265,7 +265,7 @@ Proof.
{ apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
intros (j&?&Hjl&_)%heap_array_lookup.
rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
rewrite loc_add_0 -fmap_seq big_sepL_fmap.
rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
setoid_rewrite <-loc_add_assoc.
rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
......
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