mention that tactic is the identity or gives error

1 files changed, 2 insertions, 35 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index cce7199338..b3b0df5c8a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4671,43 +4671,10 @@ congruence.
 \end{ErrMsgs}
 
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
 \section{Checking properties of terms}
 
+Each of the following tactics acts as the identity if the check succeeds, and results in an error otherwise.
+
 \subsection{\tt constr\_eq \term$_1$ \term$_2$}
 \tacindex{constr\_eq}
 \label{constreq}