Cleaned CHANGES (rough backport of 11855 from v8.2 to trunk).

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

1 files changed, 14 insertions, 13 deletions

diff --git a/CHANGES b/CHANGES
index 2e747ce8b..1ccda6344 100644
--- a/CHANGES
+++ b/CHANGES
@@ -43,7 +43,7 @@ Language
   statements.
 - Support for sort-polymorphism on constants denoting inductive types.
 - Several evolutions of the module system (handling of module aliases, 
-  functorial module types, an Include feature, etc). (TODO: Say more!)
+  functorial module types, an Include feature, etc).
 - Prop now a subtype of Set (predicative and impredicative forms).
 - Recursive inductive types in Prop with a single constructor of which
   all arguments are in Prop is now considered to be a singleton
@@ -210,10 +210,9 @@ Notations, coercions, implicit arguments and type inference
 - New modifier in "Implicit Arguments" to force an implicit argument to
   be maximally inserted.
 - New modifier of "Implicit Arguments" to enrich the set of implicit arguments.
-  (DOC TODO?)
 - New options Global and Local to "Implicit Arguments" for section
   surviving or non export outside module.
-- Level "constr" moved from 9 to 8. (DOC TODO?)
+- Level "constr" moved from 9 to 8.
 - Structure/Record now printed as Record (unless option Printing All is set).
 - Support for parametric notations defining constants.
 - Insertion of coercions below product types refrains to unfold
@@ -224,13 +223,15 @@ Tactic Language
 
 - Second-order pattern-matching now working in Ltac "match" clauses
   (syntax for second-order unification variable is "@?X").
+- Support for matching on let bindings in match context using syntax
+  "H := body" or "H := body : type".
 - Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer).
 - The general sequence tactical "expr_0 ; [ expr_1 | ... | expr_n ]"
   is extended so that at most one expr_i may have the form "expr .."
   or just "..". Also, n can be different from the number of subgoals
   generated by expr_0. In this case, the value of expr (or idtac in
   case of just "..") is applied to the intermediate subgoals to make
-  the number of tactics equal to the number of subgoals. (DOC TODO)
+  the number of tactics equal to the number of subgoals.
 - A name used as the name of the parameter of a lemma (like f in
   "apply f_equal with (f:=t)") is now interpreted as a ltac variable
   if such a variable exists (this is a possible source of
@@ -252,7 +253,7 @@ Tactic Language
 Tactics
 
 - New tactics "apply -> term", "apply <- term", "apply -> term in
-  ident", "apply <- term in ident" for applying equivalences (iff). (DOC TODO)
+  ident", "apply <- term in ident" for applying equivalences (iff).
 - Slight improvement of the hnf and simpl tactics when applied on
   expressions with explicit occurrences of match or fix.
 - New tactics "eapply in", "erewrite", "erewrite in".
@@ -280,7 +281,7 @@ Tactics
     is still legal but equivalent to intros ?a ?b.
   * intro pattern "(A & ... & Y & Z)" synonym to "(A,....,(Y,Z)))))"
     for right-associative constructs like /\ or exists.
-- Several syntax extensions concerning "rewrite": (DOC TODO)
+- Several syntax extensions concerning "rewrite":
   * "rewrite A,B,C" can be used to rewrite A, then B, then C. These rewrites
     occur only on the first subgoal: in particular, side-conditions of the 
     "rewrite A" are not concerned by the "rewrite B,C".
@@ -474,10 +475,11 @@ Tools
 - Extended -I coqtop/coqc option to specify a logical dir: "-I dir -as coqdir".
 - New coqtop/coqc option -exclude-dir to exclude subdirs for option -R.
 - The binary "parser" has been renamed to "coq-parser".
-- Improved coqdoc and dump of globalization information to give more meta-information
-  on identifiers. All categories of Coq definitions are supported, which makes
-  typesetting trivial in the generated documentation. Support for hyperlinking
-  and indexing developments in the tex output has been implemented as well.
+- Improved coqdoc and dump of globalization information to give more 
+  meta-information on identifiers. All categories of Coq definitions are 
+  supported, which makes typesetting trivial in the generated documentation.
+  Support for hyperlinking and indexing developments in the tex output
+  has been implemented as well.
 
 Miscellaneous
 
@@ -626,7 +628,7 @@ Tactics
   juste a simple hypothesis name. For instance: 
    rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H
    rewrite H in * |-  will do try rewrite H in Hi for all hypothesis Hi <> H.
-- Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO)
+- Added "dependent rewrite term" and "dependent rewrite term in hyp".
 - Added "autorewrite with ... in hyp [using ...]".
 - Tactic "replace" now accepts a "by" tactic clause.
 - Added "clear - id" to clear all hypotheses except the ones depending in id.
@@ -905,8 +907,7 @@ Vernacular commands
 
 - "Declare ML Module" now allows to import .cma files. This avoids to use a
    bunch of "Declare ML Module" statements when using several ML files.
-- "Set Printing Width n" added, allows to change the size of width printing
-   (TODO : doc).
+- "Set Printing Width n" added, allows to change the size of width printing.
 - "Implicit Variables Type x,y:t" (new syntax: "Implicit Types x y:t")
   assigns default types for binding variables.
 - Declarations of Hints and Notation now accept a "Local" flag not to