ZArith_base, Zbool, Bool_nat

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2798 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 11 deletions

diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index 240efb6e4..f85b0bddd 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -10,16 +10,13 @@
 
 (** Library for manipulating integers based on binary encoding *)
 
-Require Export fast_integer.
-Require Export zarith_aux.
-Require Export auxiliary.
-Require Export Zsyntax.
-Require Export ZArith_dec.
-Require Export Zmisc.
-Require Export Wf_Z.
+Require Export ZArith_base.
 
-Hints Resolve Zle_n Zplus_sym Zplus_assoc Zmult_sym Zmult_assoc
-  Zero_left Zero_right Zmult_one Zplus_inverse_l Zplus_inverse_r 
-  Zmult_plus_distr_l Zmult_plus_distr_r : zarith.
+(** Extra modules using [Omega] or [Ring]. *)
 
-Require Export Zhints.
+Require Export Zcomplements.
+Require Export Zsqrt.
+Require Export Zpower.
+Require Export Zdiv.
+Require Export Zlogarithm.
+Require Export Zbool.