Added back the tactics [apply -> ident], etc. to Tactics.v after

committing the extension of the general sequence operator.


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

1 files changed, 11 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index e4e2a89bd4..ed69d91040 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,6 +9,17 @@ Tactic Language
 - Second-order pattern-matching now working in Ltac "match" clauses
   (syntax for second-order unification variable is "@?X").
 - 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.
+
+Tactics
+
+- New tactics [apply -> term], [apply <- term], [apply -> term in
+  ident], [apply <- term in ident] for applying equivalences (iff).
 
 Changes from V8.1gamma to V8.1
 ==============================