diff options
author | 2017-08-17 16:23:32 +0200 | |
---|---|---|
committer | 2017-08-17 16:23:32 +0200 | |
commit | 88226ad302d4c128173644fc9d992ada67ba6d9c (patch) | |
tree | 767960aeab21ad6d8114b05836c2f8ab5b6aa6b8 /doc | |
parent | b6ebf2c50d940e174c1860d5853d15619b0537b0 (diff) | |
parent | 7f3a7aa17cddfda15146117f7f8a6c40a91ab243 (diff) |
Merge PR #974: Change section caption, improve some wording
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-tac.tex | 62 |
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} |