From 503d92f75b520e88864649306f5a70058ff73990 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 18 Nov 2010 14:40:08 +0000
Subject: NZLog: we define log2_up, a base-2 logarithm that rounds up instead
 of down as log2

 Some more results about log2. Similar results for log2_up.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13648 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/Abstract/ZProperties.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'theories/Numbers/Integer/Abstract')

diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 2e747782c7..9a592e8ac2 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -7,11 +7,12 @@
 (************************************************************************)
 
 Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor
- ZGcd ZLcm.
+ ZGcd ZLcm NZLog NZSqrt.
 
 (** This functor summarizes all known facts about Z. *)
 
 Module Type ZProp (Z:ZAxiomsSig) :=
  ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z
- <+ NZSqrt.NZSqrtProp Z Z <+ NZLog.NZLog2Prop Z Z Z
+ <+ NZSqrtProp Z Z
+ <+ NZLog2Prop Z Z Z <+ NZLog2UpProp Z Z Z
  <+ ZDivProp Z <+ ZQuotProp Z <+ ZGcdProp Z <+ ZLcmProp Z.
-- 
cgit v1.2.3