From e3ac2c2f97fc6d9fe2909b88a3de2846b0fa9e5d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Aug 2022 10:01:50 -0400
Subject: [PATCH] update std++
---
coq-iris.opam | 2 +-
iris/algebra/list.v | 4 ++--
iris_unstable/algebra/list.v | 6 +++---
3 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/coq-iris.opam b/coq-iris.opam
index 39b99c3cb..c7b397154 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
depends: [
"coq" { (>= "8.13" & < "8.16~") | (= "dev") }
- "coq-stdpp" { (= "dev.2022-08-11.0.66a28855") | (= "dev") }
+ "coq-stdpp" { (= "dev.2022-08-11.3.67890e47") | (= "dev") }
]
build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 07f48e154..039c2d751 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -158,11 +158,11 @@ Next Obligation.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
- apply list_fmap_equiv_ext=>y. apply oFunctor_map_id.
+ apply list_fmap_equiv_ext=>???. apply oFunctor_map_id.
Qed.
Next Obligation.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
- apply list_fmap_equiv_ext=>y; apply oFunctor_map_compose.
+ apply list_fmap_equiv_ext=>???; apply oFunctor_map_compose.
Qed.
Global Instance listOF_contractive F :
diff --git a/iris_unstable/algebra/list.v b/iris_unstable/algebra/list.v
index 0afcf8c30..ee55e1a16 100644
--- a/iris_unstable/algebra/list.v
+++ b/iris_unstable/algebra/list.v
@@ -526,7 +526,7 @@ Proof.
- intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
by apply (cmra_morphism_validN (fmap f : option A → option B)).
- intros l. apply Some_proper. rewrite -!list_fmap_compose.
- apply list_fmap_equiv_ext, cmra_morphism_core, _.
+ apply list_fmap_equiv_ext=>???. apply cmra_morphism_core, _.
- intros l1 l2. apply list_equiv_lookup=>i.
by rewrite list_lookup_op !list_lookup_fmap list_lookup_op cmra_morphism_op.
Qed.
@@ -540,11 +540,11 @@ Next Obligation.
Qed.
Next Obligation.
intros F A ? B ? x. rewrite /= -{2}(list_fmap_id x).
- apply list_fmap_equiv_ext=>y. apply urFunctor_map_id.
+ apply list_fmap_equiv_ext=>???. apply urFunctor_map_id.
Qed.
Next Obligation.
intros F A1 ? A2 ? A3 ? B1 ? B2 ? B3 ? f g f' g' x. rewrite /= -list_fmap_compose.
- apply list_fmap_equiv_ext=>y; apply urFunctor_map_compose.
+ apply list_fmap_equiv_ext=>???; apply urFunctor_map_compose.
Qed.
Global Instance listURF_contractive F :
--
GitLab