1 files changed, 13 insertions, 49 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b13ae9b7b..b3b0df5c8 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4671,50 +4671,15 @@ congruence.
 \end{ErrMsgs}
 
 
+\section{Checking properties of terms}
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-\section{Everything after this point has yet to be sorted}
-
+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}
 
-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 +4687,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 +4703,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 +4713,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 +4723,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}