From fdea9174359868bd9d4f3cf397243c0be921f0d8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 4 Nov 2014 19:50:02 +0100
Subject: Documenting the change of semantics of the replace tactic.

---
 CHANGES                   | 1 +
 doc/refman/RefMan-tac.tex | 5 ++++-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/CHANGES b/CHANGES
index 767ecf2e11..8a90f0965f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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}
 
-- 
cgit v1.2.3