Suppression de Rsyntax en v8

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

4 files changed, 9 insertions, 18 deletions

diff --git a/Makefile b/Makefile
index be3a3e1a1..7ad21c5da 100644
--- a/Makefile
+++ b/Makefile
@@ -649,7 +649,7 @@ WELLFOUNDEDVO=\
  theories/Wellfounded/Lexicographic_Product.vo 
 
 REALSBASEVO=\
- theories/Reals/Rdefinitions.vo theories/Reals/Rsyntax.vo \
+ theories/Reals/Rdefinitions.vo \
  theories/Reals/Raxioms.vo      theories/Reals/RIneq.vo \
  theories/Reals/DiscrR.vo       theories/Reals/Rbase.vo \
 
@@ -792,7 +792,8 @@ NEWCONTRIBVO=$(CONTRIBVO)
 OBSOLETETHEORIESVO=\
  theories7/Lists/PolyList.vo theories7/Lists/PolyListSyntax.vo \
  theories7/ZArith/Zsyntax.vo \
- theories7/ZArith/zarith_aux.vo	theories7/ZArith/fast_integer.vo
+ theories7/ZArith/zarith_aux.vo	theories7/ZArith/fast_integer.vo \
+ theories7/Reals/Rsyntax.vo
 
 OLDINITVO=$(INITVO:theories%.vo=theories7%.vo)
 OLDTHEORIESVO=$(THEORIESVO:theories%.vo=theories7%.vo) $(OBSOLETETHEORIESVO)
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 62de585bc..ef1044449 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -13,8 +13,8 @@
 (*********************************************************)
 
 Require Export ZArith_base.
-Require Export Rsyntax. Open Local Scope R_scope.
-
+Require Export Rdefinitions.
+Open Local Scope R_scope.
 
 (*********************************************************)
 (*               Field axioms                            *)
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
deleted file mode 100644
index b453ef9db..000000000
--- a/theories/Reals/Rsyntax.v
+++ /dev/null
@@ -1,13 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-(*i $Id$ i*)
-
-Require Export Rdefinitions.
-
-Axiom NRplus : R -> R.
-Axiom NRmult : R -> R.
diff --git a/theories7/Reals/Raxioms.v b/theories7/Reals/Raxioms.v
index 4516a206f..4c26b1ed0 100644
--- a/theories7/Reals/Raxioms.v
+++ b/theories7/Reals/Raxioms.v
@@ -13,8 +13,11 @@
 (*********************************************************)
 
 Require Export ZArith_base.
+V7only [
 Require Export Rsyntax.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+Import R_scope.
+].
+Open Local Scope R_scope.
 
 V7only [
 (*********************************************************)