diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Reals/ConstructiveRIneq.v (renamed from theories/Reals/RIneq_constr.v) | 0 | ||||
| -rw-r--r-- | theories/Reals/ConstructiveRcomplete.v (renamed from theories/Reals/Rcomplete_constr.v) | 2 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 2 |
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. |