From 8525692feee0f2aec9af488d1986ba8141f053dc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 14 Nov 2003 18:46:33 +0000
Subject: Inclusion de Zbool qui contient une partie de Zmisc dans ZArith_base

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4914 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/ZArith/ZArith_base.v | 1 +
 theories/ZArith/Zbool.v       | 7 ++++++-
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 7123e3449e..97f4c3f3ed 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -28,6 +28,7 @@ Require Export Znat.
 Require Export auxiliary.
 Require Export Zsyntax.
 Require Export ZArith_dec.
+Require Export Zbool.
 Require Export Zmisc.
 Require Export Wf_Z.
 
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 1b1ca455fd..fcbdd1141f 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -8,7 +8,12 @@
 
 (* $Id$ *)
 
-Require ZArith_base.
+Require BinInt.
+Require Zeven.
+Require Zorder.
+Require Zcompare.
+Require ZArith_dec.
+Require Zsyntax.
 Require Sumbool.
 
 (** The decidability of equality and order relations over
-- 
cgit v1.2.3