Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 0 insertions, 32 deletions

diff --git a/theories7/Reals/Reals.v b/theories7/Reals/Reals.v
deleted file mode 100644
index d0f879ab..00000000
--- a/theories7/Reals/Reals.v
+++ /dev/null
@@ -1,32 +0,0 @@
-(************************************************************************)
-(*  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: Reals.v,v 1.1.2.1 2004/07/16 19:31:34 herbelin Exp $ i*)
-
-(* The library REALS is divided in 6 parts :
-   - Rbase: basic lemmas on R
-            equalities and inequalities
-            Ring and Field are instantiated on R
-   - Rfunctions: some useful functions (Rabsolu, Rmin, Rmax, fact...)
-   - SeqSeries: theory of sequences and series
-   - Rtrigo: theory of trigonometric functions
-   - Ranalysis: some topology and general results of real analysis (mean value theorem, intermediate value theorem,...)
-   - Integration: Newton and Riemann' integrals
-
-  Tactics are:
-  - DiscrR: for goals like ``?1<>0``
-  - Sup: for goals like ``?1<?2``
-  - RCompute: for equalities with constants like ``10*10==100``
-  - Reg: for goals like (continuity_pt ?1 ?2) or (derivable_pt ?1 ?2) *)
-  
-Require Export Rbase.
-Require Export Rfunctions.
-Require Export SeqSeries.
-Require Export Rtrigo.
-Require Export Ranalysis.
-Require Export Integration.