From 70b30af7df05921be85e84a32c02694b5503e1ef Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 3 Oct 2023 14:05:36 +0200
Subject: [PATCH] update dependencies

---
 coq-iris.opam       |  2 +-
 iris/algebra/csum.v | 10 +++++-----
 iris/algebra/gmap.v |  2 +-
 iris/algebra/ofe.v  |  6 +++---
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/coq-iris.opam b/coq-iris.opam
index e88b35623..2a1ba6e3f 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.16" & < "8.19~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2023-09-21.2.7f6df4fa") | (= "dev") }
+  "coq-stdpp" { (= "dev.2023-10-03.0.83c8fcbf") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/csum.v b/iris/algebra/csum.v
index 3a76de354..70e09f061 100644
--- a/iris/algebra/csum.v
+++ b/iris/algebra/csum.v
@@ -65,8 +65,8 @@ Proof.
   split.
   - intros mx my; split.
     + by destruct 1; constructor; try apply equiv_dist.
-    + intros Hxy; feed inversion (Hxy 0); subst; constructor; try done;
-      apply equiv_dist=> n; by feed inversion (Hxy n).
+    + intros Hxy; oinversion (Hxy 0); subst; constructor; try done;
+      apply equiv_dist=> n; by oinversion (Hxy n).
   - intros n; split.
     + by intros [|a|]; constructor.
     + by destruct 1; constructor.
@@ -91,7 +91,7 @@ Global Program Instance csum_cofe `{!Cofe A, !Cofe B} : Cofe csumO :=
   {| compl := csum_compl |}.
 Next Obligation.
   intros ?? n c; rewrite /compl /csum_compl.
-  feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
+  oinversion (chain_cauchy c 0 n); first auto with lia; constructor.
   + rewrite (conv_compl n (csum_chain_l c _)) /=. destruct (c n); naive_solver.
   + rewrite (conv_compl n (csum_chain_r c _)) /=. destruct (c n); naive_solver.
 Qed.
@@ -239,9 +239,9 @@ Proof.
       constructor; eauto using cmra_pcore_l.
   - intros [a|b|] ? [=]; subst; auto.
     + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
-      feed inversion (cmra_pcore_idemp a ca); repeat constructor; auto.
+      oinversion (cmra_pcore_idemp a ca); repeat constructor; auto.
     + destruct (pcore b) as [cb|] eqn:?; simplify_option_eq.
-      feed inversion (cmra_pcore_idemp b cb); repeat constructor; auto.
+      oinversion (cmra_pcore_idemp b cb); repeat constructor; auto.
   - intros x y ? [->|[(a&a'&->&->&?)|(b&b'&->&->&?)]]%csum_included [=].
     + exists CsumBot. rewrite csum_included; eauto.
     + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index ead5b1e59..fed922c7f 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -34,7 +34,7 @@ Global Program Instance gmap_cofe `{Cofe A} : Cofe gmapO :=
   {| compl := gmap_compl |}.
 Next Obligation.
   intros ? n c k. rewrite /compl /gmap_compl map_lookup_imap.
-  feed inversion (λ H, chain_cauchy c 0 n H k);simplify_option_eq;auto with lia.
+  oinversion (λ H, chain_cauchy c 0 n H k);simplify_option_eq;auto with lia.
   by rewrite conv_compl /=; apply reflexive_eq.
 Qed.
 
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 2c0a4098f..d64a63f82 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1076,7 +1076,7 @@ Section sum.
     { compl := sum_compl }.
   Next Obligation.
     intros ?? n c; rewrite /compl /sum_compl.
-    feed inversion (chain_cauchy c 0 n); first by si_solver.
+    oinversion (chain_cauchy c 0 n); first by si_solver.
     - rewrite (conv_compl n (inl_chain c _)) /=. destruct (c n); naive_solver.
     - rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver.
   Qed.
@@ -1230,7 +1230,7 @@ Section option.
     split.
     - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
       intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist.
-      by intros n; feed inversion (Hxy n).
+      by intros n; oinversion (Hxy n).
     - apply _.
     - destruct 1; constructor; eauto using dist_le with si_solver.
   Qed.
@@ -1245,7 +1245,7 @@ Section option.
     { compl := option_compl }.
   Next Obligation.
     intros ? n c; rewrite /compl /option_compl.
-    feed inversion (chain_cauchy c 0 n); auto with lia; [].
+    oinversion (chain_cauchy c 0 n); auto with lia; [].
     constructor. rewrite (conv_compl n (option_chain c _)) /=.
     destruct (c n); naive_solver.
   Qed.
-- 
GitLab