Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom

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

4 files changed, 8 insertions, 2 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index b076de2aff..c522e01b3e 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -18,3 +18,5 @@ Require Export Between.
 Require Export Peano_dec.
 Require Export Compare_dec.
 Require Export Factorial.
+
+Require Export ArithRing.
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index 3e64980cb7..d86d7f1169 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import Arith.
+Require Import Le.
 
 Open Local Scope nat_scope.
 
diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v
index a37387792b..5a2eeda484 100644
--- a/theories/NArith/NArith.v
+++ b/theories/NArith/NArith.v
@@ -11,4 +11,6 @@
 (** Library for binary natural numbers *)
 
 Require Export BinPos.
-Require Export BinNat.
\ No newline at end of file
+Require Export BinNat.
+
+Require Export NArithRing.
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index 169a253fe6..5747afc9a2 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -19,3 +19,5 @@ Require Export Zsqrt.
 Require Export Zpower.
 Require Export Zdiv.
 Require Export Zlogarithm.
+
+Export ZArithRing.