diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index e06457fe46..675c2bf174 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3841,6 +3841,26 @@ this tactic. % En attente d'un moyen de valoriser les fichiers de demos %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v} +\subsection{\tt easy} +\tacindex{easy} +\label{easy} + +This tactic tries to solve the current goal by a number of standard closing steps. +In particular, it tries to close the current goal using the closing tactics +{\tt trivial}, reflexivity, symmetry, contradiction and inversion of hypothesis. +If this fails, it tries introducing variables and splitting and-hypotheses, +using the closing tactics afterwards, and splitting the goal using {\tt split} and recursing. + +This tactic solves goals that belong to many common classes; in particular, many cases of +unsatisfiable hypotheses, and simple equality goals are usually solved by this tactic. + +\begin{Variant} +\item {\tt now \tac} + \tacindex{now} + + Run \tac\/ followed by easy. This is a notation for {\tt \tac; easy}. +\end{Variant} + \section{Controlling automation} \subsection{The hints databases for {\tt auto} and {\tt eauto}} |