diff options
| -rw-r--r-- | Makefile | 5 | ||||
| -rw-r--r-- | theories/Reals/Raxioms.v | 4 | ||||
| -rw-r--r-- | theories/Reals/Rsyntax.v | 13 | ||||
| -rw-r--r-- | theories7/Reals/Raxioms.v | 5 |
4 files changed, 9 insertions, 18 deletions
@@ -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 62de585bcc..ef10444493 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 b453ef9dbd..0000000000 --- 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 4516a206f8..4c26b1ed02 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 [ (*********************************************************) |