ajout de mes modifs recentes

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

1 files changed, 49 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index 8dbbd45b0..e9d0c0265 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,8 @@ Syntax
 - No more support for version 7 syntax and for translation to version 8 syntax.
 - Support for primitive interpretation of string literals
 - Extended support for Unicode ranges (Unicode doc TODO)
+- In fixpoints, the { struct ... } annotation is not mandatory any more when 
+  only one of the arguments has an inductive type (doc TODO) 
 
 Environment variables
 
@@ -43,11 +45,22 @@ Tactics
   setoid_symmetry, setoid_transitivity, setoid_reflexivity and autorewite).
   New syntax for declaring relations and morphisms (old syntax still working
   with minor modifications, but deprecated) (doc TODO)
+- When rewriting H where H is not directly a Coq equality, search first H for 
+  a registered setoid equality before starting to reduce in H. This is unlikely 
+  to break any script. Should this happen nonetheless, one can insert manually 
+  some "unfold ... in H" before rewriting.
+- Fixed various bugs about (setoid) rewrite ... in ... (in particular #1101)
+- "rewrite ... in" now accepts a clause as place where to rewrite instead of 
+  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 
+  (doc TODO)
 - Added "clear - id" to clear all hypotheses except the ones depending in id.
 - Added "dependent rewrite term" and "dependent rewrite term in hyp" (doc TODO)
 - The argument of Declare Left Step and Declare Right Step is now a term
   (it used to be a reference) (doc TODO)
 - Omega now handles arbitrary precision integers
+- Several bug fixes in Reflexive Omega (romega). 
 - Idtac can now be left implicit in a [...|...] construct: for instance, 
   [ foo | | bar ] stands for [ foo | idtac | bar ]. (doc TODO). 
 - "Tactic Notation" extended to allow notations of tacticals (doc TODO).
@@ -72,9 +85,24 @@ Tactics
 - New definition command: "GenFixpoint" (TODO) (doc)
 - functional induction has been re-implemented from the new definition
   command (doc TODO)
-- Genralisation of induction "induction x1...xn using scheme" where
+- Generalisation of induction "induction x1...xn using scheme" where
   scheme is an induction principle with complex predicates (like the
   ones generated by function induction) (doc TODO).
+- Some small Ltac tactics has been added to the standard library 
+  (file Tactics.v)(TODO doc ?): 
+  * f_equal : instead of using the different f_equalX lemmas
+  * case_eq : a "case" without loss of information. An equality 
+     stating the current situation is generated in every sub-cases.
+  * swap : for a negated goal ~B and a negated hypothesis H:~A, 
+     swap H asks you to prove A from hypothesis B 
+  * revert : revert H is generalize H; clear H
+
+
+Extraction
+ 
+- all type parts should now disappear instead of sometimes producing _ 
+  (for instance in Map.empty).
+- TODO bug fixes...
 
 
 Modules
@@ -106,10 +134,30 @@ Libraries
   compatibility (useless hypothesys of Zgt_square_simpl and
   Zlt_square_simpl removed; fixed names mentioning letter O instead of
   digit 0; weaken premises in Z_lt_induction)
+- Znumtheory now contains a gcd function that can compute within Coq
 - More lemmas stated on Type in Wf.v, removal of redundant Fix_F
 - Coq.List.In_dec has been set transparent (this may exceptionally break
   proof scripts, set it locally opaque for compatibility)
 - Change of the internal names of lemmas in OmegaLemmas
+- List.v has been much expanded (TODO en dire plus)
+- The notion of permutation of lists has been developped, both in 
+  List.v and Permutation.v (TODO en dire plus ?)
+- New file SetoidList.v now contains results about lists seen with 
+  respect to a setoid equality. 
+- Library NArith has been expanded, mostly with results coming from 
+  Intmap (for instance a bitwise xor), plus also a bridge between N and 
+  Bitvector. 
+- A new library FSets+FMaps of finite sets and maps (TODO doc quelque part)
+  Nota: files FSetAVL and FMapAVL in this library are known to take some 
+  time to compile. On slow computers, you may choose to disable them 
+  via the Configure option --fsets no 
+- Intmap has been reorganized. In particular its address type "addr" is 
+  now N. User contributions known to use Intmap have been adapted 
+  accordingly. If you're using this library please contact us. 
+  A wrapper FMapIntMap now presents Intmap as a particular implementation 
+  of FMaps. New developments are strongly encouraged to use either this 
+  wrapper or any other implementations of FMap instead of using directly 
+  this obsolete Intmap. 
 
 Tools