From d5f49c85630e25f2c2b45cf03cc3f589e7cdaf5f Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Sun, 2 Jun 2019 17:59:15 +0200
Subject: docs: Add refman+stdlib documentation

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

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index f0ada745e7..eedd8a3d61 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -328,6 +328,19 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Integer/Binary/ZBinary.v
     theories/Numbers/Integer/NatPairs/ZNatPairs.v
     </dd>
+
+    <dt> <b>&nbsp;&nbsp;Floats</b>:
+       Floating-point arithmetic
+    </dt>
+    <dd>
+    theories/Floats/FloatClass.v
+    theories/Floats/PrimFloat.v
+    theories/Floats/SpecFloat.v
+    theories/Floats/FloatOps.v
+    theories/Floats/FloatAxioms.v
+    theories/Floats/FloatLemmas.v
+    (theories/Floats/Floats.v)
+    </dd>
     </dl>
   </dd>
 
-- 
cgit v1.2.3


From 3cb32772ccd0f2882a40d7f75b044b738adadad3 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Tue, 22 Oct 2019 11:57:16 +0200
Subject: Add extraction for primitive floats

Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
---
 doc/stdlib/hidden-files | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index bb6df87970..5b243c8a9e 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -13,6 +13,7 @@ plugins/extraction/ExtrHaskellZNum.v
 plugins/extraction/ExtrOcamlBasic.v
 plugins/extraction/ExtrOcamlBigIntConv.v
 plugins/extraction/ExtrOCamlInt63.v
+plugins/extraction/ExtrOCamlFloats.v
 plugins/extraction/ExtrOcamlIntConv.v
 plugins/extraction/ExtrOcamlNatBigInt.v
 plugins/extraction/ExtrOcamlNatInt.v
-- 
cgit v1.2.3