Réorganisation de la librairie des réels

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

1 files changed, 3 insertions, 12 deletions

diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 17aec980e..807525601 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -14,20 +14,11 @@
 (* Propriétés                                               *)
 (************************************************************)
 
-Require Rbase.
-Require DiscrR.
-Require Rbasic_fun.
+Require RealsB.
 Require Rfunctions.
-Require Rseries.
-Require Binome.
-Require AltSeries.
-Require Rcomplet.
-Require Rprod.
-Require Rtrigo_def.
-Require Rtrigo_alt.
-Require Cos_plus.
+Require SeqSeries.
+Require Rtrigo.
 Require Ranalysis1.
-Require PSeries_reg.
 Require Exp_prop.
 Require Rsqrt_def.
 Require R_sqrt.