From 04d270a46e8c481e0b1f21904c6b25f0b7359fa0 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 13 Jan 2004 15:12:46 +0000
Subject: Suppression de Rsyntax en v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5197 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile                  |  5 +++--
 theories/Reals/Raxioms.v  |  4 ++--
 theories/Reals/Rsyntax.v  | 13 -------------
 theories7/Reals/Raxioms.v |  5 ++++-
 4 files changed, 9 insertions(+), 18 deletions(-)
 delete mode 100644 theories/Reals/Rsyntax.v

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 [
 (*********************************************************)
-- 
cgit v1.2.3