Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631

3 files changed, 33 insertions, 1 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b27a4dc94..5c519e46e 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1840,6 +1840,9 @@ This is useful for declaring the implicit type of a single variable.
 \subsection{Implicit generalization
 \label{implicit-generalization}
 \comindex{Generalizable Variables}}
+% \textquoteleft since \` doesn't do what we want
+\index{0genimpl@{\textquoteleft\{\ldots\}}}
+\index{0genexpl@{\textquoteleft(\ldots)}}
 
 Implicit generalization is an automatic elaboration of a statement with
 free variables into a closed statement where these variables are
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index df0cd2b82..41ea0a5dc 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -434,6 +434,7 @@ be shortened in {\tt fun~x~y~z~:~A~=>~t}).
 \subsection{Abstractions
 \label{abstractions}
 \index{abstractions}}
+\index{fun@{{\tt fun \ldots => \ldots}}}
 
 The expression ``{\tt fun} {\ident} {\tt :} {\type} {\tt =>}~{\term}''
 defines the {\em abstraction} of the variable {\ident}, of type
@@ -455,6 +456,7 @@ occurs in the list of binders, it is expanded to a let-in definition
 \subsection{Products
 \label{products}
 \index{products}}
+\index{forall@{{\tt forall \ldots, \ldots}}}
 
 The expression ``{\tt forall}~{\ident}~{\tt :}~{\type}{\tt
 ,}~{\term}'' denotes the {\em product} of the variable {\ident} of
@@ -495,6 +497,7 @@ arguments is used for making explicit the value of implicit arguments
 \subsection{Type cast
 \label{typecast}
 \index{Cast}}
+\index{cast@{{\tt(\ldots: \ldots)}}}
 
 The expression ``{\term}~{\tt :}~{\type}'' is a type cast
 expression. It enforces the type of {\term} to be {\type}.
@@ -514,6 +517,7 @@ symbol ``\_'' and {\Coq} will guess the missing piece of information.
 \label{let-in}
 \index{Let-in definitions}
 \index{let-in}}
+\index{let@{{\tt let \ldots := \ldots in \ldots}}}
 
 
 {\tt let}~{\ident}~{\tt :=}~{\term$_1$}~{\tt in}~{\term$_2$} denotes
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a2d45046b..675c2bf17 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3523,8 +3523,13 @@ with its $\beta\iota$-normal form.
 \end{ErrMsgs}
 
 \begin{Variants}
+\item {\tt unfold {\qualid} in {\ident}}
+  \tacindex{unfold \dots in}
+
+  Replaces {\qualid} in hypothesis {\ident} with its definition
+  and replaces the hypothesis with its $\beta\iota$ normal form.
+
 \item {\tt unfold {\qualid}$_1$, \dots, \qualid$_n$}
-  \tacindex{unfold \dots\ in}
 
   Replaces {\em simultaneously} {\qualid}$_1$, \dots, {\qualid}$_n$
   with their definitions and replaces the current goal with its
@@ -3836,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}}