From 6106884157ae89378e76f37051d991fa5763c8bd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 16 Dec 2000 16:45:11 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1137 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index cf43980283..c5139f20ee 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; 
-- 
cgit v1.2.3