Fix #4846

Bug description:
The "now" tactic, which is being used in the standard library,
is not documented in the Reference Manual

This commit documents the easy tactic, and gives now
as a variant.

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}}