From b815eba9e644fc030ebc6966d7872be9a74d0967 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 18 Mar 2020 08:12:22 +0100
Subject: [PATCH] update dependencies; fix for fmap_seq rename
---
opam | 2 +-
theories/heap_lang/array.v | 2 +-
theories/heap_lang/lifting.v | 4 ++--
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/opam b/opam
index 1b8a693e2..ba44b0eae 100644
--- a/opam
+++ b/opam
@@ -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}%"]
diff --git a/theories/heap_lang/array.v b/theories/heap_lang/array.v
index 611f5623b..3a3990a95 100644
--- a/theories/heap_lang/array.v
+++ b/theories/heap_lang/array.v
@@ -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.
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 9f403fd1a..8619893ad 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -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".
--
GitLab