update sur les tactiques

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

1 files changed, 6 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 60643cd086..b7fd0b0d6a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -197,8 +197,6 @@ Extensions de syntaxe avec Grammar et Syntax
 - Le non affichage des Infix est corrigé.
 
 - Ajout d'une syntaxe pour les réels: ``Rexpr``.
-  Point noir dû aux constantes: (Rplus (Rplus (Rplus R1 R1) (Rplus R1 R1)) R1)
-  est toujours (2+2+1) au lieu de 2+2+1 
 
 
 Syntaxe des constructions
@@ -315,6 +313,12 @@ Tactiques
   La tactique a été instantiée pour les nombres réels et peut donc être
   utilisée pour résoudre des égalités sur les réels.
 
+- Nouveau: tactique Fourier qui résoud les inégalités linéaires sur les
+  nombres réels.
+
+- Nouveau: diverses tactiques pour les nombres réels: DiscrR, SplitRmult, 
+  SplitAbsolu.
+
 Outils
 
 - Deux binaires maximum : coqtop.byte et coqtop.opt si plateforme native;