From 09ca1ab6b81ae8e7955a2d2f5b5adc01e796708e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 30 Jan 2001 21:17:56 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1294 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES             | 7 +++++--
 TODO                | 1 +
 dev/changements.txt | 3 +++
 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
-- 
cgit v1.2.3