From 8c2799476f669e82ea0d49adb2a2dcec6c05e35b Mon Sep 17 00:00:00 2001
From: Paul Steckler <steck@stecksoft.com>
Date: Wed, 16 Aug 2017 11:46:33 -0400
Subject: change section caption, improve some wording

---
 doc/refman/RefMan-tac.tex | 27 ++++++++++++---------------
 1 file changed, 12 insertions(+), 15 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b13ae9b7b..cce719933 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4706,15 +4706,13 @@ congruence.
 
 
 
-\section{Everything after this point has yet to be sorted}
-
+\section{Checking properties of terms}
 
 \subsection{\tt constr\_eq \term$_1$ \term$_2$}
 \tacindex{constr\_eq}
 \label{constreq}
 
-This tactic applies to any goal. It checks whether its arguments are
-equal modulo alpha conversion and casts.
+This tactic checks whether its arguments are equal modulo alpha conversion and casts.
 
 \ErrMsg \errindex{Not equal}
 
@@ -4722,8 +4720,8 @@ equal modulo alpha conversion and casts.
 \tacindex{unify}
 \label{unify}
 
-This tactic applies to any goal. It checks whether its arguments are
-unifiable, potentially instantiating existential variables.
+This tactic checks whether its arguments are unifiable, potentially
+instantiating existential variables.
 
 \ErrMsg \errindex{Not unifiable}
 
@@ -4738,9 +4736,9 @@ unifiable, potentially instantiating existential variables.
 \tacindex{is\_evar}
 \label{isevar}
 
-This tactic applies to any goal. It checks whether its argument is an
-existential variable. Existential variables are uninstantiated
-variables generated by e.g. {\tt eapply} (see Section~\ref{apply}).
+This tactic checks whether its argument is a current existential
+variable. Existential variables are uninstantiated variables generated
+by {\tt eapply} (see Section~\ref{apply}) and some other tactics.
 
 \ErrMsg \errindex{Not an evar}
 
@@ -4748,10 +4746,9 @@ variables generated by e.g. {\tt eapply} (see Section~\ref{apply}).
 \tacindex{has\_evar}
 \label{hasevar}
 
-This tactic applies to any goal. It checks whether its argument has an
-existential variable as a subterm. Unlike {\tt context} patterns
-combined with {\tt is\_evar}, this tactic scans all subterms,
-including those under binders.
+This tactic checks whether its argument has an existential variable as
+a subterm.  Unlike {\tt context} patterns combined with {\tt is\_evar},
+this tactic scans all subterms, including those under binders.
 
 \ErrMsg \errindex{No evars}
 
@@ -4759,8 +4756,8 @@ including those under binders.
 \tacindex{is\_var}
 \label{isvar}
 
-This tactic applies to any goal. It checks whether its argument is a
-variable or hypothesis in the current goal context or in the opened sections.
+This tactic checks whether its argument is a variable or hypothesis in the
+current goal context or in the opened sections.
 
 \ErrMsg \errindex{Not a variable or hypothesis}
 
-- 
cgit v1.2.3