diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 37 |
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} |