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 <herbelin@users.noreply.github.com>

Update doc/changelog/10-standard-library/11725-cleanup-reals.rst

Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>

Update doc/changelog/10-standard-library/11725-cleanup-reals.rst

Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>

Improve notations

0 files changed, 0 insertions, 0 deletions