From a4432d05514a60f59b7917331abfb9f589d8ca85 Mon Sep 17 00:00:00 2001
From: Vincent Semeria
Date: Wed, 22 Apr 2020 19:41:20 +0200
Subject: Document Cauchy reals

---
 doc/sphinx/changes.rst | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 7401aff48c..ba1cb741ed 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -481,10 +481,12 @@ Changes in 8.11+beta1
   .. _811Reals:
 
 - **Added:**
-  Module `Reals.ConstructiveCauchyReals` defines constructive real numbers
+  Module `Reals.Cauchy.ConstructiveCauchyReals` defines constructive real numbers
   by Cauchy sequences of rational numbers
   (`#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria,
   with the help and review of Guillaume Melquiond and Bas Spitters).
+  This module is not meant to be imported directly, please import
+  `Reals.Abstract.ConstructiveReals` instead.
 - **Added:**
   New module `Reals.ClassicalDedekindReals` defines Dedekind real
   numbers as boolean-valued functions along with 3 logical axioms:
-- 
cgit v1.2.3