From 7f3a7aa17cddfda15146117f7f8a6c40a91ab243 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 16 Aug 2017 15:06:43 -0400
Subject: mention that tactic is the identity or gives error

---
 doc/refman/RefMan-tac.tex | 37 ++-----------------------------------
 1 file changed, 2 insertions(+), 35 deletions(-)

(limited to 'doc')

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}
-- 
cgit v1.2.3