- Implantation de la suggestion 1873 sur discriminate. Au final,

  discriminate/injection/simplify_eq acceptent maintenant un terme
  comme argument. Les clauses "with" et les variantes "e" sont aussi
  acceptées. Aussi, discriminate sans argument essaie maintenant
  toutes les hyps quantifiées (au lieu de traiter seulement les buts
  t1<>t2).

--This line, and those below, will be ignored--

M    doc/refman/RefMan-tac.tex
M    CHANGES
M    pretyping/evd.ml
M    pretyping/termops.ml
M    pretyping/termops.mli
M    pretyping/clenv.ml
M    tactics/extratactics.ml4
M    tactics/inv.ml
M    tactics/equality.ml
M    tactics/tactics.mli
M    tactics/equality.mli
M    tactics/tacticals.ml
M    tactics/eqdecide.ml4
M    tactics/tacinterp.ml
M    tactics/tactics.ml
M    tactics/extratactics.mli
M    toplevel/auto_ind_decl.ml
M    contrib/funind/invfun.ml
M    test-suite/success/Discriminate.v
M    test-suite/success/Injection.v
M    proofs/clenvtac.mli
M    proofs/clenvtac.ml


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

1 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 4304fce184..675db3f185 100644
--- a/CHANGES
+++ b/CHANGES
@@ -202,6 +202,9 @@ Tactics
 - 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".
+- New tactics "ediscriminate", "einjection", "esimplify_eq".
+- Tactics "discriminate", "injection", "simplify_eq" now support any
+  term as argument. Clause "with" is also supported.
 - Unfoldable references can be given by notation's string rather than by name 
   in unfold.
 - The "with" arguments are now typed using informations from the current goal: