MAJ du manuel de référence

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

1 files changed, 10 insertions, 13 deletions

diff --git a/CHANGES b/CHANGES
index fb403a5cc..7e69e8b06 100644
--- a/CHANGES
+++ b/CHANGES
@@ -57,15 +57,13 @@ Tactics
 - "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).
+   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 "autorewrite with ... in hyp [using ...]" (doc TODO).
-- Tactic "replace" now accepts a "by" tactic clause (doc TODO).
-- Added "clear - id" to clear all hypotheses except the ones depending in id
-  (doc TODO).
+- 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.
 - The argument of Declare Left Step and Declare Right Step is now a term
-  (it used to be a reference) (doc TODO).
+  (it used to be a reference).
 - Omega now handles arbitrary precision integers.
 - Several bug fixes in Reflexive Omega (romega).
 - Idtac can now be left implicit in a [...|...] construct: for instance, 
@@ -77,13 +75,12 @@ Tactics
   used to solve unresolved subterms of term arguments of tactics (doc TODO).
 - Better support for coercions to Sortclass in tactics expecting type 
   arguments.
-- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
-  (doc TODO).
+- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses.
 - New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
   (doc TODO).
-- New introduction pattern "?" for letting Coq choose a name (doc TODO).
-- Added "eassumption" (doc TODO).
-- Added option 'using lemmas' to auto, trivial and eauto (doc TODO).
+- New introduction pattern "?" for letting Coq choose a name.
+- Added "eassumption".
+- Added option 'using lemmas' to auto, trivial and eauto.
 - Tactic "congruence" is now complete for its intended scope (ground
   equalities and inequalities with constructors). Furthermore, it
   tries to equates goal and hypotheses.
@@ -95,7 +92,7 @@ Tactics
   to see hidden occurrences).
 - Generalization 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).
+  ones generated by function induction).
 - Some small Ltac tactics has been added to the standard library 
   (file Tactics.v):
   * f_equal : instead of using the different f_equalX lemmas