Slight simplification of naming of tactics in equality.ml (hopefully).

Isolating a core tactic in replace, shareable to cutrewrite.

1 files changed, 15 insertions, 8 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a3953bb968..11568bb4d3 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2680,14 +2680,6 @@ the same variants as {\tt rewrite} has.
 
 \end{Variants}
 
-
-\subsection{\tt cutrewrite -> \term$_1$ = \term$_2$}
-\label{cutrewrite}
-\tacindex{cutrewrite}
-
-This tactic acts like {\tt replace {\term$_1$} with {\term$_2$}}
-(see below).
-
 \subsection{\tt replace \term$_1$ with \term$_2$}
 \label{tactic:replace}
 \tacindex{replace \dots\ with}
@@ -2738,6 +2730,21 @@ n}| assumption || symmetry; try assumption]}.
     in the conclusion of the goal.
     The \nterm{clause} argument must not contain any \texttt{type of} nor \texttt{value of}.
 
+\item {\tt cutrewrite <- (\term$_1$ = \term$_2$)}
+%\label{cutrewrite}
+\tacindex{cutrewrite}
+
+This tactic is deprecated. It acts like {\tt replace {\term$_2$} with
+  {\term$_1$}}, or, equivalently as {\tt enough} (\term$_1$ =
+\term$_2$) {\tt as <-}.
+
+\item {\tt cutrewrite -> (\term$_1$ = \term$_2$)}
+%\label{cutrewrite}
+\tacindex{cutrewrite}
+
+This tactic is deprecated. It can be replaced by {\tt enough}
+(\term$_1$ = \term$_2$) {\tt as ->}.
+
 \end{Variants}
 
 \subsection{\tt subst \ident}