MAJ

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

1 files changed, 5 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index cf4398028..c5139f20e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -111,7 +111,8 @@ que les 3 primitives), on peut typer avec "constr", "tactic", ou
   Arguments" et non plus selon la valeur qu'elle avait au moment de la 
   définition dans la section.
 
-- SearchPattern / SearchRewrite (contrib de Yves Bertot)
+- SearchPattern / SearchRewrite (contrib from Yves Bertot); Search can
+  be restricted to some modules
 
 - Le point final des commandes doit être suivi d'un blanc (retour chariot, tabulation ou espace)
 
@@ -141,6 +142,9 @@ Tactiques
 - AutoRewrite ne s'occupe maintenant que du but principal et c'est les
   Hint Rewrite qui gèrent les sous-buts générés
 
+- Redondant or incompatible instantiations in Apply ... with now
+  correctly trapped
+
 Outils
 
 - deux binaires maximum : coqtop.byte et coqtop.opt si plateforme native;