1 files changed, 7 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index c5139f20e..d8d9f0e1b 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