MAJ

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

1 files changed, 27 insertions, 11 deletions

diff --git a/CHANGES b/CHANGES
index 08802e053..2b26c3b9d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,16 +1,12 @@
-- Consecutive as in patterns are forbidden
+Métathéorie
 
-- Names generated in Cases are different
+- Ajout de définitions locales (Let-In)
 
-- "command" in grammars is now "constr" as in pretty-printing rules
+Syntaxe des constructions
 
-- Numérotation dans l'ordre des hypothèses créées par Decompose
-- Correction de bugs (quand le type ne commence pas par un inductif)
+- Consecutive as in patterns are forbidden
 
-- Simpl ne déplie plus les appels récursifs d'un Fix mutuel réduit. En
-revanche, si une constante n'est qu'indirectement un Fix, on ne garde
-en général plus son nom (sauf dans les cas "simples"). Rem : c'est une
-source d'incompatibilité.
+- Names generated in Cases are different (source d'incompatibilité)
 
 - Davantage d'inférence automatique de "?".
 
@@ -18,6 +14,11 @@ source d'incompatibilité.
   cas de clauses par défaut redondantes auquel cas la première est prise
   avec un avertissement.
 
+Vernac
+
+- "command" in grammars and quotations is now "constr" as in
+  pretty-printing rules
+
 - Ajout de la syntaxe "[" phrase_1 ... phrase_n"]." pour grouper des
 phrases (utile pour Time et pour des grammaires abrégeant plusieurs
 commandes)
@@ -33,8 +34,23 @@ l'ast, il faut typer explicitement la grammaire avec Ast ou List
   DelPath -> Remove Path;
   Print Path -> Print Coercion Paths.
 
-- Ajout d'un Let primitif
+- Bug affichage Infix corrigé
 
-- Ajout (officiel) d'une tactique LetTac et d'un Induction "convivial"
+
+Tactiques
 
 - Langage de tactique
+
+- Ajout (officiel) d'une tactique LetTac et d'un Induction "convivial"
+
+- Decompose :
+  - Numérotation dans l'ordre des hypothèses créées
+  - Correction de bugs (quand le type ne commence pas par un inductif)
+    et refus d'agir sous les ->.
+
+- Simpl ne déplie plus les appels récursifs d'un Fix mutuel réduit. En
+  revanche, si une constante n'est qu'indirectement un Fix, on ne garde
+  en général plus son nom (sauf dans les cas "simples"). Rem : c'est une
+  source d'incompatibilité.
+
+