From 35979f40a946abbffd413953116c34b2e53e022c Mon Sep 17 00:00:00 2001
From: Columbus240 <8899730+Columbus240@users.noreply.github.com>
Date: Tue, 6 Aug 2024 18:42:15 +0200
Subject: [PATCH] Avoid functions deprecated since coq v8.16

Concerning real numbers.
---
 theories/Topology/RFuncContinuity.v  | 2 +-
 theories/Topology/RationalsInReals.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Topology/RFuncContinuity.v b/theories/Topology/RFuncContinuity.v
index 2fe4f451..7cc4d229 100644
--- 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
index ea008900..70d26f3b 100644
--- 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.