MAJ

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

1 files changed, 7 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index c5139f20ee..d8d9f0e1b9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -121,7 +121,13 @@ Tactiques
 
 - Langage de tactique Ltac
 
-- Ajout (officiel) d'une tactique LetTac et d'un Induction "convivial"
+- Tactique Let renommé en LetTac et utilise le let-in primitif;
+  Induction renommé en OldInduction et nouveau Induction plus
+  "convivial".
+
+- Elim avec un schéma d'élimination différent de celui créé à la
+  définition d'un inductif n'est plus possible. Il faut utiliser Elim
+  <hyp> with <nom du schéma d'élimination>.
 
 - Decompose :
   - Numérotation dans l'ordre des hypothèses créées