From d6ebd62341fd6bbe2b7d4e5309d8e13f786a9462 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 2 Nov 2010 15:10:43 +0000
Subject: Numbers : log2. Abstraction, properties and implementations.

 Btw, we finally declare the original Zpower as the power on Z.
 We should switch to a more efficient one someday, but in the
 meantime BigN is proved with respect to the old one.

 TODO: reform Zlogarithm with respect to Zlog_def

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13606 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/stdlib/index-list.html.template | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'doc/stdlib')

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 4f208c7da..e0f445d03 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -183,6 +183,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/ZArith/Zpow_def.v
     theories/ZArith/Zpower.v
     theories/ZArith/Zdiv.v
+    theories/ZArith/Zlog_def.v
     theories/ZArith/Zlogarithm.v
     (theories/ZArith/ZArith.v)
     theories/ZArith/Zgcd_alt.v
@@ -238,6 +239,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/NatInt/NZProperties.v
     theories/Numbers/NatInt/NZPow.v
     theories/Numbers/NatInt/NZSqrt.v
+    theories/Numbers/NatInt/NZLog.v
     </dd>
     </dt>
 
@@ -281,6 +283,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Numbers/Natural/Abstract/NParity.v
     theories/Numbers/Natural/Abstract/NPow.v
     theories/Numbers/Natural/Abstract/NSqrt.v
+    theories/Numbers/Natural/Abstract/NLog.v
     theories/Numbers/Natural/Abstract/NProperties.v
     theories/Numbers/Natural/Binary/NBinary.v
     theories/Numbers/Natural/Peano/NPeano.v
-- 
cgit v1.2.3