From b6ab00a80f271bcd5e2706471dd2bbe4894c95a6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Aug 2022 20:55:36 +0200
Subject: [PATCH] Bump stdpp.

---
 coq-iris.opam                       |  2 +-
 iris/algebra/dfrac.v                | 28 ++++++++++++++--------------
 iris/algebra/frac.v                 | 14 +++++++-------
 iris/algebra/numbers.v              |  4 ++--
 iris/algebra/ofe.v                  |  6 +++---
 iris/algebra/ufrac.v                | 10 +++++-----
 iris/base_logic/lib/ghost_var.v     |  2 +-
 iris/base_logic/lib/iprop.v         | 10 +++++-----
 iris/base_logic/lib/later_credits.v |  8 ++++----
 iris/base_logic/lib/saved_prop.v    |  2 +-
 iris/bi/lib/fractional.v            | 12 ++++++------
 iris/bi/updates.v                   |  4 ++--
 iris/program_logic/adequacy.v       |  4 ++--
 iris_heap_lang/lib/logatom_lock.v   |  6 +++---
 tests/one_shot_once.v               |  2 +-
 15 files changed, 57 insertions(+), 57 deletions(-)

diff --git a/coq-iris.opam b/coq-iris.opam
index 5e3a91ef7..dfc8afa67 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.13" & < "8.17~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2022-08-11.4.409da1f6") | (= "dev") }
+  "coq-stdpp" { (= "2022-08-12.3.d6c6e66a") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/dfrac.v b/iris/algebra/dfrac.v
index 3511d31b6..0c8c16b93 100644
--- a/iris/algebra/dfrac.v
+++ b/iris/algebra/dfrac.v
@@ -103,7 +103,7 @@ Section dfrac.
 
   Lemma dfrac_own_included q p : DfracOwn q ≼ DfracOwn p ↔ (q < p)%Qp.
   Proof.
-    rewrite Qp_lt_sum. split.
+    rewrite Qp.lt_sum. split.
     - rewrite /included /op /dfrac_op_instance. intros [[o| |?] [= ->]]. by exists o.
     - intros [o ->]. exists (DfracOwn o). by rewrite dfrac_op_own.
   Qed.
@@ -120,18 +120,18 @@ Section dfrac.
     - intros [?| |?] [?| |?] [?| |?];
         rewrite /op /dfrac_op_instance 1?assoc_L 1?assoc_L; done.
     - intros [?| |?] [?| |?];
-        rewrite /op /dfrac_op_instance 1?(comm_L Qp_add); done.
+        rewrite /op /dfrac_op_instance 1?(comm_L Qp.add); done.
     - intros [?| |?] dq; rewrite /pcore /dfrac_pcore_instance; intros [= <-];
         rewrite /op /dfrac_op_instance; done.
     - intros [?| |?] ? [= <-]; done.
     - intros [?| |?] [?| |?] ? [[?| |?] [=]] [= <-]; eexists _; split; try done;
         apply dfrac_discarded_included.
     - intros [q| |q] [q'| |q']; rewrite /op /dfrac_op_instance /valid /dfrac_valid_instance //.
-      + intros. trans (q + q')%Qp; [|done]. apply Qp_le_add_l.
-      + apply Qp_lt_le_incl.
-      + intros. trans (q + q')%Qp; [|by apply Qp_lt_le_incl]. apply Qp_le_add_l.
-      + intros. trans (q + q')%Qp; [|done]. apply Qp_lt_add_l.
-      + intros. trans (q + q')%Qp; [|done]. apply Qp_lt_add_l.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp.le_add_l.
+      + apply Qp.lt_le_incl.
+      + intros. trans (q + q')%Qp; [|by apply Qp.lt_le_incl]. apply Qp.le_add_l.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
+      + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
   Qed.
   Canonical Structure dfracR := discreteR dfrac dfrac_ra_mixin.
 
@@ -142,19 +142,19 @@ Section dfrac.
   Proof.
     intros [q| |q];
       rewrite /op /cmra_op -cmra_discrete_valid_iff /valid /cmra_valid //=.
-    - apply Qp_not_add_le_l.
-    - move=> /Qp_lt_le_incl. apply Qp_not_add_le_l.
+    - apply Qp.not_add_le_l.
+    - move=> /Qp.lt_le_incl. apply Qp.not_add_le_l.
   Qed.
 
   Global Instance dfrac_cancelable q : Cancelable (DfracOwn q).
   Proof.
     apply: discrete_cancelable.
     intros [q1| |q1][q2| |q2] _ [=]; simplify_eq/=; try done.
-    - by destruct (Qp_add_id_free q q2).
-    - by destruct (Qp_add_id_free q q1).
+    - by destruct (Qp.add_id_free q q2).
+    - by destruct (Qp.add_id_free q q1).
   Qed.
   Global Instance dfrac_own_id_free q : IdFree (DfracOwn q).
-  Proof. intros [q'| |q'] _ [=]. by apply (Qp_add_id_free q q'). Qed.
+  Proof. intros [q'| |q'] _ [=]. by apply (Qp.add_id_free q q'). Qed.
   Global Instance dfrac_discarded_core_id : CoreId DfracDiscarded.
   Proof. by constructor. Qed.
 
@@ -166,8 +166,8 @@ Section dfrac.
   Lemma dfrac_valid_own_r dq q : ✓ (dq ⋅ DfracOwn q) → (q < 1)%Qp.
   Proof.
     destruct dq as [q'| |q']; [|done|].
-    - apply Qp_lt_le_trans, Qp_lt_add_r.
-    - intro Hlt. etrans; last apply Hlt. apply Qp_lt_add_r.
+    - apply Qp.lt_le_trans, Qp.lt_add_r.
+    - intro Hlt. etrans; last apply Hlt. apply Qp.lt_add_r.
   Qed.
 
   Lemma dfrac_valid_own_l dq q : ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
diff --git a/iris/algebra/frac.v b/iris/algebra/frac.v
index 0747d5a1e..8072915ee 100644
--- a/iris/algebra/frac.v
+++ b/iris/algebra/frac.v
@@ -26,32 +26,32 @@ Section frac.
   Lemma frac_op p q : p â‹… q = (p + q)%Qp.
   Proof. done. Qed.
   Lemma frac_included p q : p ≼ q ↔ (p < q)%Qp.
-  Proof. by rewrite Qp_lt_sum. Qed.
+  Proof. by rewrite Qp.lt_sum. Qed.
 
   Corollary frac_included_weak p q : p ≼ q → (p ≤ q)%Qp.
-  Proof. rewrite frac_included. apply Qp_lt_le_incl. Qed.
+  Proof. rewrite frac_included. apply Qp.lt_le_incl. Qed.
 
   Definition frac_ra_mixin : RAMixin frac.
   Proof.
     split; try apply _; try done.
     intros p q. rewrite !frac_valid frac_op=> ?.
-    trans (p + q)%Qp; last done. apply Qp_le_add_l.
+    trans (p + q)%Qp; last done. apply Qp.le_add_l.
   Qed.
   Canonical Structure fracR := discreteR frac frac_ra_mixin.
 
   Global Instance frac_cmra_discrete : CmraDiscrete fracR.
   Proof. apply discrete_cmra_discrete. Qed.
   Global Instance frac_full_exclusive : Exclusive 1%Qp.
-  Proof. intros p. apply Qp_not_add_le_l. Qed.
+  Proof. intros p. apply Qp.not_add_le_l. Qed.
   Global Instance frac_cancelable (q : frac) : Cancelable q.
-  Proof. intros n p1 p2 _. apply (inj (Qp_add q)). Qed.
+  Proof. intros n p1 p2 _. apply (inj (Qp.add q)). Qed.
   Global Instance frac_id_free (q : frac) : IdFree q.
-  Proof. intros p _. apply Qp_add_id_free. Qed.
+  Proof. intros p _. apply Qp.add_id_free. Qed.
 
   (* This one has a higher precendence than [is_op_op] so we get a [+] instead
      of an [â‹…]. *)
   Global Instance frac_is_op q1 q2 : IsOp (q1 + q2)%Qp q1 q2 | 10.
   Proof. done. Qed.
   Global Instance is_op_frac q : IsOp' q (q/2)%Qp (q/2)%Qp.
-  Proof. by rewrite /IsOp' /IsOp frac_op Qp_div_2. Qed.
+  Proof. by rewrite /IsOp' /IsOp frac_op Qp.div_2. Qed.
 End frac.
diff --git a/iris/algebra/numbers.v b/iris/algebra/numbers.v
index 751285832..7acc8c125 100644
--- a/iris/algebra/numbers.v
+++ b/iris/algebra/numbers.v
@@ -9,7 +9,7 @@ Section nat.
   Local Instance nat_op_instance : Op nat := plus.
   Definition nat_op x y : x â‹… y = x + y := eq_refl.
   Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
-  Proof. by rewrite nat_le_sum. Qed.
+  Proof. by rewrite Nat.le_sum. Qed.
   Lemma nat_ra_mixin : RAMixin nat.
   Proof.
     apply ra_total_mixin; try by eauto.
@@ -165,7 +165,7 @@ Section positive.
   Local Instance pos_op_instance : Op positive := Pos.add.
   Definition pos_op_add x y : x â‹… y = (x + y)%positive := eq_refl.
   Lemma pos_included (x y : positive) : x ≼ y ↔ (x < y)%positive.
-  Proof. by rewrite Plt_sum. Qed.
+  Proof. by rewrite Pos.lt_sum. Qed.
   Lemma pos_ra_mixin : RAMixin positive.
   Proof.
     split; try by eauto.
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index e74c57758..61c1f1717 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -398,7 +398,7 @@ Section fixpoint.
     { apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar.
       induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. }
     rewrite -(fixpoint_unique fp2) //.
-    apply Hlim=> n /=. by apply Nat_iter_ind.
+    apply Hlim=> n /=. by apply Nat.iter_ind.
   Qed.
 End fixpoint.
 
@@ -440,7 +440,7 @@ Section fixpointK.
   Lemma fixpointK_unfold : fixpointK k f ≡ f (fixpointK k f).
   Proof.
     symmetry. rewrite /fixpointK. apply fixpoint_unique.
-    by rewrite -Nat_iter_S_r Nat_iter_S -fixpoint_unfold.
+    by rewrite -Nat.iter_succ_r Nat.iter_succ -fixpoint_unfold.
   Qed.
 
   Lemma fixpointK_unique (x : A) : x ≡ f x → x ≡ fixpointK k f.
@@ -471,7 +471,7 @@ Section fixpointK.
     P (fixpointK k f).
   Proof.
     intros. rewrite /fixpointK. apply fixpoint_ind; eauto.
-    intros; apply Nat_iter_ind; auto.
+    intros; apply Nat.iter_ind; auto.
   Qed.
 End fixpointK.
 
diff --git a/iris/algebra/ufrac.v b/iris/algebra/ufrac.v
index 66adffbcb..e3ee45c72 100644
--- a/iris/algebra/ufrac.v
+++ b/iris/algebra/ufrac.v
@@ -21,10 +21,10 @@ Section ufrac.
   Lemma ufrac_op p q : p â‹… q = (p + q)%Qp.
   Proof. done. Qed.
   Lemma ufrac_included p q : p ≼ q ↔ (p < q)%Qp.
-  Proof. by rewrite Qp_lt_sum. Qed.
+  Proof. by rewrite Qp.lt_sum. Qed.
 
   Corollary ufrac_included_weak p q : p ≼ q → (p ≤ q)%Qp.
-  Proof. rewrite ufrac_included. apply Qp_lt_le_incl. Qed.
+  Proof. rewrite ufrac_included. apply Qp.lt_le_incl. Qed.
 
   Definition ufrac_ra_mixin : RAMixin ufrac.
   Proof. split; try apply _; try done. Qed.
@@ -34,10 +34,10 @@ Section ufrac.
   Proof. apply discrete_cmra_discrete. Qed.
 
   Global Instance ufrac_cancelable q : Cancelable q.
-  Proof. intros n p1 p2 _. apply (inj (Qp_add q)). Qed.
+  Proof. intros n p1 p2 _. apply (inj (Qp.add q)). Qed.
   Global Instance ufrac_id_free q : IdFree q.
-  Proof. intros p _. apply Qp_add_id_free. Qed.
+  Proof. intros p _. apply Qp.add_id_free. Qed.
 
   Global Instance is_op_ufrac q : IsOp' q (q/2)%Qp (q/2)%Qp.
-  Proof. by rewrite /IsOp' /IsOp ufrac_op Qp_div_2. Qed.
+  Proof. by rewrite /IsOp' /IsOp ufrac_op Qp.div_2. Qed.
 End ufrac.
diff --git a/iris/base_logic/lib/ghost_var.v b/iris/base_logic/lib/ghost_var.v
index 448b0d3f3..56e720fd2 100644
--- a/iris/base_logic/lib/ghost_var.v
+++ b/iris/base_logic/lib/ghost_var.v
@@ -88,7 +88,7 @@ Section lemmas.
     ghost_var γ (1/2) a1 -∗
     ghost_var γ (1/2) a2 ==∗
     ghost_var γ (1/2) b ∗ ghost_var γ (1/2) b.
-  Proof. iApply ghost_var_update_2. apply Qp_half_half. Qed.
+  Proof. iApply ghost_var_update_2. apply Qp.half_half. Qed.
 
   (** Framing support *)
   Global Instance frame_ghost_var p γ a q1 q2 RES :
diff --git a/iris/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
index fb2663030..16babcffa 100644
--- a/iris/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -67,7 +67,7 @@ Module gFunctors.
 
   Definition app (Σ1 Σ2 : gFunctors) : gFunctors :=
     GFunctors (gFunctors_len Σ1 + gFunctors_len Σ2)
-              (fin_plus_inv _ (gFunctors_lookup Σ1) (gFunctors_lookup Σ2)).
+              (fin_add_inv _ (gFunctors_lookup Σ1) (gFunctors_lookup Σ2)).
 End gFunctors.
 
 Coercion gFunctors.singleton : gFunctor >-> gFunctors.
@@ -99,8 +99,8 @@ Global Hint Mode subG ! + : typeclass_instances.
 Lemma subG_inv Σ1 Σ2 Σ : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
 Proof.
   move=> H; split.
-  - move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_plus_inv_L; eauto.
-  - move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_plus_inv_R; eauto.
+  - move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_add_inv_l; eauto.
+  - move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_add_inv_r; eauto.
 Qed.
 
 Global Instance subG_refl Σ : subG Σ Σ.
@@ -108,12 +108,12 @@ Proof. move=> i; by exists i. Qed.
 Global Instance subG_app_l Σ Σ1 Σ2 : subG Σ Σ1 → subG Σ (gFunctors.app Σ1 Σ2).
 Proof.
   move=> H i; move: H=> /(_ i) [j ?].
-  exists (Fin.L _ j). by rewrite /= fin_plus_inv_L.
+  exists (Fin.L _ j). by rewrite /= fin_add_inv_l.
 Qed.
 Global Instance subG_app_r Σ Σ1 Σ2 : subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
 Proof.
   move=> H i; move: H=> /(_ i) [j ?].
-  exists (Fin.R _ j). by rewrite /= fin_plus_inv_R.
+  exists (Fin.R _ j). by rewrite /= fin_add_inv_r.
 Qed.
 
 
diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index de2dec96f..c54a4e46f 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -92,7 +92,7 @@ Section later_credit_theory.
   Lemma lc_weaken {n} m :
     m ≤ n → £ n -∗ £ m.
   Proof.
-    intros [k ->]%nat_le_sum. rewrite lc_split. iIntros "[$ _]".
+    intros [k ->]%Nat.le_sum. rewrite lc_split. iIntros "[$ _]".
   Qed.
 
   Global Instance lc_timeless n : Timeless (£ n).
@@ -281,8 +281,8 @@ Module le_upd.
         + iModIntro. iDestruct "Hupd" as (m Hstep) "[Hown Hupd]". iNext.
           iPoseProof (IH with "Hown Hupd") as "Hit"; first done.
           clear IH.
-          assert (m ≤ n) as [k ->]%nat_le_sum by lia.
-          rewrite Nat.add_comm Nat_iter_add.
+          assert (m ≤ n) as [k ->]%Nat.le_sum by lia.
+          rewrite Nat.add_comm Nat.iter_add.
           iApply iter_modal_intro.
           { by iIntros (Q) "$". }
           iApply (iter_modal_mono with "[] Hit").
@@ -297,7 +297,7 @@ Module le_upd.
       Nat.iter (S n) (λ Q, |==> ▷ Q) P.
     Proof.
       iIntros "Hlc Hupd". iPoseProof (le_upd_elim with "Hlc Hupd") as "Hit".
-      rewrite Nat_iter_S_r. iApply (iter_modal_mono with "[] Hit").
+      rewrite Nat.iter_succ_r. iApply (iter_modal_mono with "[] Hit").
       { clear. iIntros (P Q) "Hent HP". by iApply "Hent". }
       iIntros "Hupd". iMod "Hupd". iModIntro. iMod "Hupd".
       iNext. iDestruct "Hupd" as "[%m (_ & _ & $)]".
diff --git a/iris/base_logic/lib/saved_prop.v b/iris/base_logic/lib/saved_prop.v
index a2515d89d..23bbf4a06 100644
--- a/iris/base_logic/lib/saved_prop.v
+++ b/iris/base_logic/lib/saved_prop.v
@@ -107,7 +107,7 @@ Section saved_anything.
     saved_anything_own γ (DfracOwn (1/2)) x1 -∗
     saved_anything_own γ (DfracOwn (1/2)) x2 ==∗
     saved_anything_own γ (DfracOwn (1/2)) y ∗ saved_anything_own γ (DfracOwn (1/2)) y.
-  Proof. iApply saved_anything_update_2. apply Qp_half_half. Qed.
+  Proof. iApply saved_anything_update_2. apply Qp.half_half. Qed.
 End saved_anything.
 
 (** Provide specialized versions of this for convenience. **)
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 935a206e7..2303c1c31 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -55,7 +55,7 @@ Section fractional.
   Lemma fractional_half P P12 Φ q :
     AsFractional P Φ q → AsFractional P12 Φ (q/2) →
     P ⊣⊢ P12 ∗ P12.
-  Proof. by rewrite -{1}(Qp_div_2 q)=>-[->->][-> _]. Qed.
+  Proof. by rewrite -{1}(Qp.div_2 q)=>-[->->][-> _]. Qed.
   Lemma fractional_half_1 P P12 Φ q :
     AsFractional P Φ q → AsFractional P12 Φ (q/2) →
     P -∗ P12 ∗ P12.
@@ -117,12 +117,12 @@ Section fractional.
   Global Instance mul_fractional_l Φ Ψ p :
     (∀ q, AsFractional (Φ q) Ψ (q * p)) → Fractional Φ.
   Proof.
-    intros H q q'. rewrite ->!as_fractional, Qp_mul_add_distr_r. by apply H.
+    intros H q q'. rewrite ->!as_fractional, Qp.mul_add_distr_r. by apply H.
   Qed.
   Global Instance mul_fractional_r Φ Ψ p :
     (∀ q, AsFractional (Φ q) Ψ (p * q)) → Fractional Φ.
   Proof.
-    intros H q q'. rewrite ->!as_fractional, Qp_mul_add_distr_l. by apply H.
+    intros H q q'. rewrite ->!as_fractional, Qp.mul_add_distr_l. by apply H.
   Qed.
 
   (* REMARK: These two instances do not work in either direction of the
@@ -156,11 +156,11 @@ Section fractional.
   Global Instance from_sep_fractional_half_fwd P Q Φ q :
     AsFractional P Φ q → AsFractional Q Φ (q/2) →
     FromSep P Q Q | 10.
-  Proof. by rewrite /FromSep -{1}(Qp_div_2 q)=>-[-> ->] [-> _]. Qed.
+  Proof. by rewrite /FromSep -{1}(Qp.div_2 q)=>-[-> ->] [-> _]. Qed.
   Global Instance from_sep_fractional_half_bwd P Q Φ q :
     AsFractional P Φ (q/2) → AsFractional Q Φ q →
     FromSep Q P P.
-  Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed.
+  Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp.div_2. Qed.
 
   Global Instance into_sep_fractional P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
@@ -207,6 +207,6 @@ Section fractional.
     - rewrite fractional /Frame /MakeSep=><-<-. by rewrite assoc.
     - rewrite fractional /Frame /MakeSep=><-<-=>_.
       by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
-    - move=>-[-> _]->. by rewrite bi.intuitionistically_if_elim -fractional Qp_div_2.
+    - move=>-[-> _]->. by rewrite bi.intuitionistically_if_elim -fractional Qp.div_2.
   Qed.
 End fractional.
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index fdd9aa030..2db589017 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -520,7 +520,7 @@ Section fupd_derived.
   Lemma step_fupdN_S_fupd n E P :
     (|={E}[∅]▷=>^(S n) P) ⊣⊢ (|={E}[∅]▷=>^(S n) |={E}=> P).
   Proof.
-    apply (anti_symm (⊢)); rewrite !Nat_iter_S_r; apply step_fupdN_mono;
+    apply (anti_symm (⊢)); rewrite !Nat.iter_succ_r; apply step_fupdN_mono;
       rewrite -step_fupd_fupd //.
   Qed.
 
@@ -618,7 +618,7 @@ Section fupd_derived.
     Proof.
       induction n as [|n IH].
       - by rewrite -fupd_intro -except_0_intro.
-      - rewrite Nat_iter_S step_fupd_fupd IH !fupd_trans step_fupd_plain.
+      - rewrite Nat.iter_succ step_fupd_fupd IH !fupd_trans step_fupd_plain.
         apply fupd_mono. destruct n as [|n]; simpl.
         * by rewrite except_0_idemp.
         * by rewrite except_0_later.
diff --git a/iris/program_logic/adequacy.v b/iris/program_logic/adequacy.v
index bf9cd4c33..ae781fa79 100644
--- a/iris/program_logic/adequacy.v
+++ b/iris/program_logic/adequacy.v
@@ -74,14 +74,14 @@ Proof.
   { inversion_clear 1; iIntros "? ? ?"; iExists 0=> /=.
     rewrite Nat.add_0_r right_id_L. iFrame. by iApply fupd_mask_subseteq. }
   iIntros (Hsteps) "Hσ Hcred He". inversion_clear Hsteps as [|?? [t1' σ1']].
-  rewrite -(assoc_L (++)) Nat_iter_add -{1}plus_Sn_m plus_n_Sm.
+  rewrite -(assoc_L (++)) Nat.iter_add -{1}plus_Sn_m plus_n_Sm.
   rewrite lc_split. iDestruct "Hcred" as "[Hc1 Hc2]".
   iDestruct (wptp_step with "Hσ Hc1 He") as (nt') ">H"; first eauto; simplify_eq.
   iModIntro. iApply step_fupdN_S_fupd. iApply (step_fupdN_wand with "H").
   iIntros ">(Hσ & He)". iMod (IH with "Hσ Hc2 He") as "IH"; first done. iModIntro.
   iApply (step_fupdN_wand with "IH"). iIntros ">IH".
   iDestruct "IH" as (nt'') "[??]".
-  rewrite -Nat.add_assoc -(assoc_L app) -replicate_plus. by eauto with iFrame.
+  rewrite -Nat.add_assoc -(assoc_L app) -replicate_add. by eauto with iFrame.
 Qed.
 
 Lemma wp_not_stuck κs nt e σ ns Φ :
diff --git a/iris_heap_lang/lib/logatom_lock.v b/iris_heap_lang/lib/logatom_lock.v
index 61dc2888e..40dbfa74e 100644
--- a/iris_heap_lang/lib/logatom_lock.v
+++ b/iris_heap_lang/lib/logatom_lock.v
@@ -62,7 +62,7 @@ Section tada.
     iIntros (Φ) "_ HΦ".
     iMod (ghost_var_alloc Free) as (γvar) "Hvar".
     replace 1%Qp with (3/4 + 1/4)%Qp; last first.
-    { rewrite Qp_three_quarter_quarter //. }
+    { rewrite Qp.three_quarter_quarter //. }
     iDestruct "Hvar" as "[Hvar1 Hvar2]".
     wp_apply (l.(newlock_spec) with "Hvar2").
     iIntros (lk γlock) "Hlock".
@@ -82,7 +82,7 @@ Section tada.
     iMod "AU" as (s) "[[Hvar2 _] [_ Hclose]]".
     iDestruct (ghost_var_agree with "Hvar1 Hvar2") as %<-.
     iMod (ghost_var_update_2 Locked with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
-    { rewrite Qp_quarter_three_quarter //. }
+    { rewrite Qp.quarter_three_quarter //. }
     iMod ("Hclose" with "[$Hvar2 $Hlocked $Hvar1]"). done.
   Qed.
 
@@ -95,7 +95,7 @@ Section tada.
     iIntros "#Hislock %Φ AU". iApply fupd_wp.
     iMod "AU" as "[[Hvar1 [Hlocked Hvar2]] [_ Hclose]]".
     iMod (ghost_var_update_2 Free with "Hvar1 Hvar2") as "[Hvar1 Hvar2]".
-    { rewrite Qp_three_quarter_quarter //. }
+    { rewrite Qp.three_quarter_quarter //. }
     iMod ("Hclose" with "[$Hvar1]"). iModIntro.
     wp_apply (l.(release_spec) with "[$Hislock $Hlocked $Hvar2]").
     auto.
diff --git a/tests/one_shot_once.v b/tests/one_shot_once.v
index 506ac4cc7..0a7457419 100644
--- a/tests/one_shot_once.v
+++ b/tests/one_shot_once.v
@@ -49,7 +49,7 @@ Local Hint Extern 0 (environments.envs_entails _ (one_shot_inv _ _)) =>
 Lemma pending_split γ q :
   own γ (Pending q) ⊣⊢ own γ (Pending (q/2)) ∗ own γ (Pending (q/2)).
 Proof.
-  rewrite /Pending. rewrite -own_op -Cinl_op. rewrite frac_op Qp_div_2 //.
+  rewrite /Pending. rewrite -own_op -Cinl_op. rewrite frac_op Qp.div_2 //.
 Qed.
 
 Lemma pending_shoot γ n :
-- 
GitLab