One (last?) more update of CHANGES.

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

1 files changed, 53 insertions, 11 deletions

diff --git a/CHANGES b/CHANGES
index b6b937ab7f..0473a978ba 100644
--- a/CHANGES
+++ b/CHANGES
@@ -78,7 +78,7 @@ Libraries (DOC TO CHECK)
   lemmas).
 - Many changes in FSets/FMaps. In practice, compatibility with earlier
   version should be fairly good, but some adaptations may be required.
-  * Interfaces of unordered ("weak") and ordered sets has been factorized
+  * Interfaces of unordered ("weak") and ordered sets have been factorized
     thanks to new features of Coq modules (in particular Include), see
     FSetInterface. Same for maps. Hints in these interfaces have been
     reworked (they are now placed in a "set" database). 
@@ -204,16 +204,28 @@ Tactics
 - Tactics elim, case, destruct and induction now support variants eelim,
   ecase, edestruct and einduction.
 - Tactics destruct and induction now support option "with".
-- New intro pattern "?A", which genererates a fresh name based on A.
-  Caveat about a slight loss of compatibility:
-  Some intro patterns don't need space between them. In particular
-  intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
-  is still legal but equivalent to intros ?a ?b.
-- New intro pattern "(A & ... & Y & Z)" synonym to "(A,....,(Y,Z)))))"
-  for right-associative constructs like /\ or exists.
-- rewrite now supports "by" to solve side-conditions and "at" to select
-  occurrences. (DOC TODO)
-- New syntax "rewrite A,B" for "rewrite A; rewrite B"
+- Some new intro patterns: 
+  * intro pattern "?A" genererates a fresh name based on A. 
+    Caveat about a slight loss of compatibility:
+    Some intro patterns don't need space between them. In particular
+    intros ?a?b used to be legal and equivalent to intros ? a ? b. Now it
+    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)
+  * "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".
+  * "rewrite A by tac" allows to apply tac on all side-conditions generated by 
+    the "rewrite A".
+  * "rewrite A at n" allows to select occurrences to rewrite: rewrite only 
+    happen at the n-th exact occurrence of the first successful matching of
+    A in the goal. 
+  * "rewrite 3 A" or "rewrite 3!A" is equivalent to "rewrite A,A,A".
+  * "rewrite !A" means rewriting A as long as possible (and at least once).
+  * "rewrite 3?A" means rewriting A at most three times.
+  * "rewrite ?A" means rewriting A as long as possible (possibly never).
+  * many of the above extensions can be combined with each other.  
 - New syntax "rename a into b, c into d" for "rename a into b; rename c into d"
 - New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]"
   to do induction-inversion on instantiated inductive families à la BasicElim.
@@ -226,6 +238,23 @@ Tactics
   matching lemma among the components of the conjunction; tactic apply also
   able to apply lemmas of conclusion an empty type.
 - Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)".
+- New tactic "specialize H with a" or "specialize (H a)" allows to transform
+  in-place a universally-quantified hypothesis (H : forall x, T x) into its 
+  instantiated form (H : T a). Nota: "specialize" was in fact there in earlier
+  versions of Coq, but was undocumented, and had a slightly different behavior.
+- New tactic "contradict H" can be used to solve any kind of goal as long as
+  the user can provide afterwards a proof of the negation of the hypothesis H.
+  If H is already a negation, say ~T, then a proof of T is asked.
+  If the current goal is a negation, say ~U, then U is saved in H afterwards,
+  hence this new tactic "contradict" extends earlier tactic "swap", which is 
+  now obsolete. 
+- tactics f_equal is now done in ML instead of Ltac: it now works on any 
+  equality of functions, regardless of the arity of the function. 
+- some more debug of reflexive omega (romega), and internal clarifications. 
+  Moreover, romega now has a variant "romega with *" that can be also used
+  on non-Z goals (nat, N, positive) via a call to a translation tactic named
+  zify (its purpose is to Z-ify your goal...). This zify may also be used
+  independantly of romega. 
 
 Program
 
@@ -327,6 +356,19 @@ Setoid rewriting
   occurrences to rewrite, and both use the [setoid_rewrite] code, even when
   rewriting with leibniz equality if occurrences are specified.
 
+Extraction
+
+- Improved behavior of the Caml extraction of modules: name clashes should 
+  not happen anymore. 
+- The command Extract Inductive has now a syntax for infix notations. This
+  allows in particular to map Coq lists and pairs onto Caml ones:  
+    Extract Inductive list => list [ "[]" "(::)" ].
+    Extract Inductive prod => "(*)" [ "(,)" ].
+- In pattern matchings, a default pattern "| _ -> ..." is now used whenever 
+  possible if several branches are identical. For instance, functions
+  corresponding to decidability of equalities are now linear instead of 
+  quadratic.
+
 Tools
 
 - New stand-alone .vo files verifier "coqchk".