MAJ

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

3 files changed, 9 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 04650b0aff..34093e18d9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,8 +1,11 @@
 Différences V7.0beta / V7.0
 
 - Ajout de déclarations locales aux Record (record à la Randy).
-
-- Correction de bugs (Identity Coercion; Rel not in scope of ?).
+- Correction de bugs (Identity Coercion; Rel not in scope of ?;
+  implicits in inductive defs).
+- Prise en compte noms longs dans Hints et Coercions
+- Rétablissement des @Definition and co
+- Rétablissement des token extensibles et mélangeant symboles et lettres
 
 ----------------------------------------------------------------------
 English version of changes is available on
diff --git a/TODO b/TODO
index 137a7643b6..12a7b66f00 100644
--- a/TODO
+++ b/TODO
@@ -39,3 +39,4 @@ Doc:
 - clarifier la sémantique de Decompose (i.e. travaille pas sous les ->)
 - faut-il mieux spécifier la sémantique de Simpl (??)
 - vérifier si Print Table id est à jour
+- documenter @Definition and co
diff --git a/dev/changements.txt b/dev/changements.txt
index 00bfa46637..cc5025c9c3 100644
--- a/dev/changements.txt
+++ b/dev/changements.txt
@@ -156,6 +156,9 @@ Changements dans les fonctions :
         ex-Tradevar, maintenant Evarutil
           mt_tycon            -> empty_tycon
 
+        Recordops
+          struc_info          -> find_structure
+
 Changements dans les inductifs
 ------------------------------
 Nouveaux types "constructor" et "inductive" dans Term