diff options
| author | Vincent Semeria | 2019-07-26 18:40:46 +0200 |
|---|---|---|
| committer | Vincent Semeria | 2019-07-26 18:40:46 +0200 |
| commit | c9efc722c559ca315dda890cf2d5cc8e934b8ad2 (patch) | |
| tree | 0aeeab9cbc5cc59d9161e3684e2da7f5cc9b4f0d | |
| parent | a1359ffb3d95686f6176b1d4a893f16252fc745c (diff) | |
Fix typo
| -rw-r--r-- | theories/Reals/ConstructiveCauchyReals.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/ConstructiveCauchyReals.v b/theories/Reals/ConstructiveCauchyReals.v index f1d62ab6f0..5a0f4abec7 100644 --- a/theories/Reals/ConstructiveCauchyReals.v +++ b/theories/Reals/ConstructiveCauchyReals.v @@ -19,11 +19,11 @@ Open Scope Q. (* The constructive Cauchy real numbers, ie the Cauchy sequences of rational numbers. This file is not supposed to be imported, except in Rdefinitions.v, Raxioms.v, Rcomplete_constr.v - and RIneq_constr.v. + and ConstructiveRIneq.v. Constructive real numbers should be considered abstractly, - forgetting the fact that they are implemented are rational sequences. - All useful lemmas of this file are exposed in RIneq_constr.v, + forgetting the fact that they are implemented as rational sequences. + All useful lemmas of this file are exposed in ConstructiveRIneq.v, under more abstract names, like Rlt_asym instead of CRealLt_asym. *) |