From beeb3ed57c4749ff84524250a8b79dfa0b1e2f78 Mon Sep 17 00:00:00 2001
From: Vincent Semeria
Date: Wed, 28 Aug 2019 00:21:26 +0200
Subject: Define morphisms of real numbers and accelerate Cauchy reals

Prove that morphisms preserve additions

Fix stdlib index

Prove that constructive real morphisms preserve multiplications by integers

Prove that constructive real morphisms preserve multiplications by rationals

Prove CReal_mult_pos_appart_zero

Prove that constructive real morphisms preserve multiplications

Prove that constructive real morphisms preserve divisions

Rewrite convergence in sort Prop, to extract smaller programs

Rewrite convergence on integers, to extract smaller programs

Fix typos
---
 doc/stdlib/index-list.html.template | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index cc91776a4d..d1b98b94a3 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -515,7 +515,9 @@ through the <tt>Require Import</tt> command.</p>
   <dd>
     theories/Reals/Rdefinitions.v
     theories/Reals/ConstructiveReals.v
+    theories/Reals/ConstructiveRealsMorphisms.v
     theories/Reals/ConstructiveCauchyReals.v
+    theories/Reals/ConstructiveCauchyRealsMult.v
     theories/Reals/Raxioms.v
     theories/Reals/ConstructiveRIneq.v
     theories/Reals/ConstructiveRealsLUB.v
-- 
cgit v1.2.3