Rename ConstructiveRIneq and ConstructiveRcomplete

3 files changed, 2 insertions, 2 deletions

diff --git a/theories/Reals/RIneq_constr.v b/theories/Reals/ConstructiveRIneq.v
index adffa9b719..adffa9b719 100644
--- a/theories/Reals/RIneq_constr.v
+++ b/theories/Reals/ConstructiveRIneq.v
diff --git a/theories/Reals/Rcomplete_constr.v b/theories/Reals/ConstructiveRcomplete.v
index 5db6dcd49d..9fb98a528b 100644
--- a/theories/Reals/Rcomplete_constr.v
+++ b/theories/Reals/ConstructiveRcomplete.v
@@ -12,7 +12,7 @@
 Require Import QArith_base.
 Require Import Qabs.
 Require Import ConstructiveCauchyReals.
-Require Import RIneq_constr.
+Require Import ConstructiveRIneq.
 
 Local Open Scope R_scope_constr.
 
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index a479d7c1a3..72475b79d7 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -13,7 +13,7 @@
 (** * Basic lemmas for the classical real numbers        *)
 (*********************************************************)
 
-Require Import RIneq_constr.
+Require Import ConstructiveRIneq.
 Require Export Raxioms.
 Require Import Rpow_def.
 Require Import Zpower.