simplif de la partie ML de ring/field

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

3 files changed, 22 insertions, 12 deletions

diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index c522e01b3..18dbd27f9 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -8,15 +8,5 @@
 
 (*i $Id$ i*)
 
-Require Export Le.
-Require Export Lt.
-Require Export Plus.
-Require Export Gt.
-Require Export Minus.
-Require Export Mult.
-Require Export Between.
-Require Export Peano_dec.
-Require Export Compare_dec.
-Require Export Factorial.
-
+Require Export Arith_base.
 Require Export ArithRing.
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
new file mode 100644
index 000000000..b076de2af
--- /dev/null
+++ b/theories/Arith/Arith_base.v
@@ -0,0 +1,20 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+Require Export Le.
+Require Export Lt.
+Require Export Plus.
+Require Export Gt.
+Require Export Minus.
+Require Export Mult.
+Require Export Between.
+Require Export Peano_dec.
+Require Export Compare_dec.
+Require Export Factorial.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index 77fa80539..6f8a5f127 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -16,7 +16,7 @@ Notation not_eq_sym := sym_not_eq.
 
 Implicit Types m n p q : nat.
 
-Require Import Arith.
+Require Import Arith_base.
 Require Import Peano_dec.
 Require Import Compare_dec.