From ad91d136b8d51e859ce3b959674757818e753bcb Mon Sep 17 00:00:00 2001 From: Vincent Semeria Date: Sun, 1 Mar 2020 17:30:57 +0100 Subject: Cleanup stdlib reals. Use implicit arguments for ConstructiveReals. Move ConstructiveReals into new directory Abstract. Remove imports of implementations inside those Abstract files. Add changelog for constructive reals cleanup Move Cauchy reals into new directory Cauchy Update stdlib index Rename sum_f_R0 Use coqdoc comments Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin Update doc/changelog/10-standard-library/11725-cleanup-reals.rst Co-Authored-By: Hugo Herbelin Improve notations --- .../10-standard-library/11725-cleanup-reals.rst | 6 ++++++ doc/stdlib/index-list.html.template | 16 ++++++++++------ 2 files changed, 16 insertions(+), 6 deletions(-) create mode 100644 doc/changelog/10-standard-library/11725-cleanup-reals.rst (limited to 'doc') diff --git a/doc/changelog/10-standard-library/11725-cleanup-reals.rst b/doc/changelog/10-standard-library/11725-cleanup-reals.rst new file mode 100644 index 0000000000..84a8ceb514 --- /dev/null +++ b/doc/changelog/10-standard-library/11725-cleanup-reals.rst @@ -0,0 +1,6 @@ +- **Changed:** +Use implicit arguments for ``ConstructiveReals``. Move ``ConstructiveReals`` + into new directory ``Abstract``. Remove imports of implementations inside + those ``Abstract`` files. Move implementation by means of Cauchy sequences in new directory ``Cauchy``. + (`#11725 `_, + by Vincent Semeria). diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 0f05237036..e64b4be454 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -528,13 +528,17 @@ through the Require Import command.

theories/Reals/Rdefinitions.v - theories/Reals/ConstructiveReals.v - theories/Reals/ConstructiveRealsMorphisms.v - theories/Reals/ConstructiveCauchyReals.v - theories/Reals/ConstructiveCauchyRealsMult.v + theories/Reals/Cauchy/ConstructiveCauchyReals.v + theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v + theories/Reals/Cauchy/ConstructiveCauchyAbs.v theories/Reals/ClassicalDedekindReals.v theories/Reals/Raxioms.v - theories/Reals/ConstructiveRealsLUB.v + theories/Reals/Abstract/ConstructiveReals.v + theories/Reals/Abstract/ConstructiveRealsMorphisms.v + theories/Reals/Abstract/ConstructiveLUB.v + theories/Reals/Abstract/ConstructiveAbs.v + theories/Reals/Abstract/ConstructiveLimits.v + theories/Reals/Abstract/ConstructiveSum.v theories/Reals/RIneq.v theories/Reals/DiscrR.v theories/Reals/ROrderedType.v @@ -579,7 +583,7 @@ through the Require Import command.

theories/Reals/Ranalysis5.v theories/Reals/Ranalysis_reg.v theories/Reals/Rcomplete.v - theories/Reals/ConstructiveRcomplete.v + theories/Reals/Cauchy/ConstructiveRcomplete.v theories/Reals/RiemannInt.v theories/Reals/RiemannInt_SF.v theories/Reals/Rpow_def.v -- cgit v1.2.3