diff options
Diffstat (limited to 'theories/Reals/Cauchy/ConstructiveCauchyReals.v')
| -rw-r--r-- | theories/Reals/Cauchy/ConstructiveCauchyReals.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Reals/Cauchy/ConstructiveCauchyReals.v b/theories/Reals/Cauchy/ConstructiveCauchyReals.v index 70574f6135..b332457a7b 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyReals.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyReals.v @@ -39,6 +39,8 @@ Require CMorphisms. WARNING: this module is not meant to be imported directly, please import `Reals.Abstract.ConstructiveReals` instead. + + WARNING: this file is experimental and likely to change in future releases. *) Definition QCauchySeq (un : positive -> Q) : Prop |