commit de field + renommages

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

8 files changed, 4 insertions, 4 deletions

diff --git a/contrib/ring/ArithRing.v b/contrib/ring/LegacyArithRing.v
index 959d66c749..959d66c749 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/LegacyArithRing.v
diff --git a/contrib/ring/NArithRing.v b/contrib/ring/LegacyNArithRing.v
index ee9fb37615..ee9fb37615 100644
--- a/contrib/ring/NArithRing.v
+++ b/contrib/ring/LegacyNArithRing.v
diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v
index 667e24d535..dc8635bdf9 100644
--- a/contrib/ring/LegacyRing.v
+++ b/contrib/ring/LegacyRing.v
@@ -9,7 +9,7 @@
 (* $Id: Ring.v 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 Require Export Bool.
-Require Export Ring_theory.
+Require Export LegacyRing_theory.
 Require Export Quote.
 Require Export Ring_normalize.
 Require Export Ring_abstract.
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/LegacyRing_theory.v
index 192ff1f571..192ff1f571 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/LegacyRing_theory.v
diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/LegacyZArithRing.v
index 075431827c..075431827c 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/LegacyZArithRing.v
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 574c24421f..28de54e658 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Import Ring_theory.
+Require Import LegacyRing_theory.
 Require Import Quote.
 Require Import Ring_normalize.
 
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 6d0d057780..199ae75721 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Import Ring_theory.
+Require Import LegacyRing_theory.
 Require Import Quote.
 
 Set Implicit Arguments.
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 1c5121ef69..e81c9ddd5c 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -43,7 +43,7 @@ let ring_dir = ["Coq";"ring"]
 let setoids_dir = ["Coq";"Setoids"]
 
 let ring_constant = Coqlib.gen_constant_in_modules "Ring"
-  [ring_dir@["Ring_theory"];
+  [ring_dir@["LegacyRing_theory"];
    ring_dir@["Setoid_ring_theory"];
    ring_dir@["Ring_normalize"];
    ring_dir@["Ring_abstract"];