Documentation du contenu de REALS

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

1 files changed, 16 insertions, 0 deletions

diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
index 9bce35b28..db6df635c 100644
--- a/theories/Reals/Reals.v
+++ b/theories/Reals/Reals.v
@@ -8,6 +8,22 @@
 
 (*i $Id$ 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.