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