From c690a68ba0b78b913cbcb60f7508d431071d4c79 Mon Sep 17 00:00:00 2001
From: Vincent Semeria
Date: Fri, 4 Oct 2019 18:29:58 +0200
Subject: Replace classical reals quotient axioms by functional extensionality.
 Define homotopy propositions and homotopy sets. Rename local variable R in
 test Nsatz, to avoid a name collision with the type of real numbers.

---
 doc/changelog/10-standard-library/10827-dedekind-reals.rst | 11 +++++++++++
 doc/stdlib/index-list.html.template                        |  3 ++-
 2 files changed, 13 insertions(+), 1 deletion(-)
 create mode 100644 doc/changelog/10-standard-library/10827-dedekind-reals.rst

(limited to 'doc')

diff --git a/doc/changelog/10-standard-library/10827-dedekind-reals.rst b/doc/changelog/10-standard-library/10827-dedekind-reals.rst
new file mode 100644
index 0000000000..5d8467025b
--- /dev/null
+++ b/doc/changelog/10-standard-library/10827-dedekind-reals.rst
@@ -0,0 +1,11 @@
+- New module `Reals.ClassicalDedekindReals` defines Dedekind real numbers
+  as boolean-values functions along with 3 logical axioms: limited principle
+  of omniscience, excluded middle of negations and functional extensionality.
+  The exposed type :g:`R` in module :g:`Reals.Rdefinitions` is those
+  Dedekind reals, hidden behind an opaque module.
+  Classical Dedekind reals are a quotient of constructive reals, which allows
+  to transport many constructive proofs to the classical case.
+
+  See `#10827 <https://github.com/coq/coq/pull/10827>`_, by Vincent Semeria,
+  based on discussions with Guillaume Melquiond, Bas Spitters and Hugo Herbelin,
+  code review by Hugo Herbelin.
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index d1b98b94a3..df7cda9aad 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -68,6 +68,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/WKL.v
     theories/Logic/FinFun.v
     theories/Logic/PropFacts.v
+    theories/Logic/HLevels.v
   </dd>
 
   <dt> <b>Structures</b>:
@@ -518,8 +519,8 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/ConstructiveRealsMorphisms.v
     theories/Reals/ConstructiveCauchyReals.v
     theories/Reals/ConstructiveCauchyRealsMult.v
+    theories/Reals/ClassicalDedekindReals.v
     theories/Reals/Raxioms.v
-    theories/Reals/ConstructiveRIneq.v
     theories/Reals/ConstructiveRealsLUB.v
     theories/Reals/RIneq.v
     theories/Reals/DiscrR.v
-- 
cgit v1.2.3