Avoid functions deprecated since coq v8.16

Concerning real numbers.
coq-community · Aug 6, 2024 · 9e45c9b · 9e45c9b
1 parent c354a0f
commit 9e45c9b
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/theories/Topology/RFuncContinuity.v b/theories/Topology/RFuncContinuity.v
@@ -311,7 +311,7 @@ assert (forall x:R, -1 < x / (1 + Rabs x) < 1).
   { pose proof (Rabs_pos x). lra. }
   apply and_comm, Rabs_def2.
   unfold Rdiv.
-  rewrite Rabs_mult, Rabs_Rinv; try lra.
+  rewrite Rabs_mult, Rabs_inv; try lra.
   rewrite (Rabs_right (1 + Rabs x)); [ | now left ].
   pattern 1 at 2.
   replace 1 with ((1 + Rabs x) * / (1 + Rabs x)) by (field; lra).

diff --git a/theories/Topology/RationalsInReals.v b/theories/Topology/RationalsInReals.v
@@ -25,7 +25,7 @@ Proof.
       apply lt_0_IZR in H0.
       now apply Z.lt_gt.
     - pattern eps at 2.
-      rewrite <- Rinv_involutive; auto with real;
+      rewrite <- Rinv_inv; auto with real;
         apply Rinv_lt_contravar; auto with real;
         apply Rmult_lt_0_compat; auto with real;
         apply Rlt_trans with (/ eps); auto with real.