MAJ

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

2 files changed, 15 insertions, 3 deletions

diff --git a/CHANGES b/CHANGES
index 0452542024..ad84d5d3d6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,12 @@
 Changes from ??? to V7.1
 ========================
 
+Language
+
+- Automatic insertion of patterns for local definitions in the type of
+  the constructors of an inductive types (for compatibility with V6.3
+  let-in style)
+
 Tactics
 
 - New tactic "ClearBody H" to clear the body of definitions in local context
@@ -16,6 +22,8 @@ Bugs
 - Bug with recursive inductive types involving let-in fixed
 - Confusion between implicit args of locals and globals of same base name fixed
 - NatRing works (to check)
+- "Discriminate 1", "Injection 1", "Simplify_eq 1" now working
+
 
 ----------------------------------------------------------------------------
 Changes from V6.3.1 and V7.0 to V7.1
diff --git a/TODO b/TODO
index 92e86c2c27..55f3d10e47 100644
--- a/TODO
+++ b/TODO
@@ -23,15 +23,19 @@ Grammaires:
 
 Doc:
 
+- Mettre à jour les messages d'erreurs de Discriminate/Simplify_eq/Injection
+- Documenter le nouvel Assert x:=t.
+- Documenter le filtrage sur les types inductifs avec let-ins (dont la
+  compatibility V6)
+
 - Ajouter let dans les règles du CIC
   -> FAIT, mais reste a documenter le let dans les inductifs
   et les champs manifestes dans les Record   
-- une passe sur le chapitre extensions de syntaxe
 - revoir le chapitre sur les tactiques utilisateur 
 - faut-il mieux spécifier la sémantique de Simpl (??)
 - documenter @Definition and co
 
 - Suggestions de la formation
-	Dans le Intros pattern on pourrait interpreter les _ 
-comme des hypotheses sur lesquelles on ferait Clear immediatement
+  Dans le Intros pattern on pourrait interpreter les _ 
+  comme des hypotheses sur lesquelles on ferait Clear immediatement
 -> FAIT, semble-t'il