diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 5 |
2 files changed, 5 insertions, 1 deletions
@@ -217,6 +217,7 @@ Tactics - non-dependent destruct/induction on an hypothesis with premisses in an inductive type with indices is fixed - residual local definitions are now correctly removed. +- The replace tactic may now replace variables in parallel. Program diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index fc6a318e6c..30ba4acf09 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1068,7 +1068,10 @@ unchanged. \item {\tt rename {\ident$_1$} into {\ident$_2$}, \ldots, {\ident$_{2k-1}$} into {\ident$_{2k}$}} -This is equivalent to the sequence of the corresponding atomic {\tt rename}. +This renames the variables {\ident$_1$} \ldots {\ident$_2k-1$} into respectively +{\ident$_2$} \ldots {\ident$_2k$} in parallel. In particular, the target +identifiers may contain identifiers that exist in the source context, as long +as the latter are also renamed by the same tactic. \end{Variants} |