aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authordesmettr2003-01-22 17:20:21 +0000
committerdesmettr2003-01-22 17:20:21 +0000
commit1297d8d77b7746f414a629e36e464cd5b53ee505 (patch)
treed7a5e95309164015555ea736ed8b15f81fa75470
parentb173ec0accede3b3aba740d1e6c54ce9679bee9c (diff)
Changements dans REALS
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3592 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--CHANGES4
1 files changed, 3 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index aa4f348273..040f050c80 100644
--- a/CHANGES
+++ b/CHANGES
@@ -34,7 +34,9 @@ Library
notations. They now must be applied (incompatibilities only in
unrealistic cases).
- More efficient versions of Zmult and times (30% faster)
-- Reals (Olivier)
+- Reals: the library is now divided in 6 parts (Rbase, Rfunctions,
+ SeqSeries, Rtrigo, Ranalysis, Integration). New tactics: Sup and
+ RCompute. See Reals.v for details.
Modules