6 files changed, 68 insertions, 32 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 0dbfe05d48..2695c5eee4 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -883,56 +883,60 @@ the type $V$ satisfies the nested positivity condition for $X$
 \settowidth\framecharacterwidth{\hh}
 \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth}
 \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}}
+\newcommand{\NatTree}{\mbox{\textsf{nattree}}}
+\newcommand{\NatTreeA}{\mbox{\textsf{nattree}}~\ensuremath{A}}
+\newcommand{\cnode}{\mbox{\textsf{node}}}
+\newcommand{\cleaf}{\mbox{\textsf{leaf}}}
 
-\noindent For instance, if one considers the type
+\noindent For instance, if one considers the following variant of a tree type branching over the natural numbers
 
 \begin{verbatim}
-Inductive tree (A:Type) : Type :=
- | leaf : list A
- | node : A -> (nat -> tree A) -> tree A
+Inductive nattree (A:Type) : Type :=
+ | leaf : nattree A
+ | node : A -> (nat -> nattree A) -> nattree A
 \end{verbatim}
 
 \begin{latexonly}
-\noindent Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$\\
+\noindent Then every instantiated constructor of $\NatTreeA$ satisfies the nested positivity condition for $\NatTree$\\
 \noindent
 \ws\ws\vv\\
-\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\
-\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\
-\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\
-\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\
+\ws\ws\vh\hh\ws concerning type $\NatTreeA$ of constructor $\cleaf$:\\
+\ws\ws\vv\ws\ws\ws\ws Type $\NatTreeA$ of constructor $\cleaf$ satisfies the positivity condition for $\NatTree$\\
+\ws\ws\vv\ws\ws\ws\ws because $\NatTree$ does not appear in any (real) arguments of the type of that constructor\\
+\ws\ws\vv\ws\ws\ws\ws (primarily because $\NatTree$ does not have any (real) arguments)\ruleref1\\
 \ws\ws\vv\\
-\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\
-\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\
-\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\
+\ws\ws\hv\hh\ws concerning type $\forall~A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$:\\
+    \ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$\\
+\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\NatTree$ because:\\
 \ws\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\
+\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\Type$\ruleref1\\
 \ws\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\
+\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $A$\ruleref1\\
 \ws\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\
+    \ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\NN\ra\NatTreeA$\ruleref{3+2}\\
 \ws\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1
+\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\NatTree$ satisfies the positivity condition for $\NatTreeA$\ruleref1
 \end{latexonly}
 \begin{rawhtml}
 <pre>
-<span style="font-family:serif">Then every instantiated constructor of <span style="font-family:monospace">list A</span> satisfies the nested positivity condition for <span style="font-family:monospace">list</span></span>
+<span style="font-family:serif">Then every instantiated constructor of <span style="font-family:monospace">nattree A</span> satisfies the nested positivity condition for <span style="font-family:monospace">nattree</span></span>
   │
-  ├─ <span style="font-family:serif">concerning type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span>:</span>
-  │    <span style="font-family:serif">Type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span> satisfies the positivity condition for <span style="font-family:monospace">list</span></span>
-  │    <span style="font-family:serif">because <span style="font-family:monospace">list</span> does not appear in any (real) arguments of the type of that constructor</span>
-  │    <span style="font-family:serif">(primarily because list does not have any (real) arguments) ... <span style="font-style:italic">(bullet 1)</span></span>
+  ├─ <span style="font-family:serif">concerning type <span style="font-family:monospace">nattree A</span> of constructor <span style="font-family:monospace">nil</span>:</span>
+  │    <span style="font-family:serif">Type <span style="font-family:monospace">nattree A</span> of constructor <span style="font-family:monospace">nil</span> satisfies the positivity condition for <span style="font-family:monospace">nattree</span></span>
+  │    <span style="font-family:serif">because <span style="font-family:monospace">nattree</span> does not appear in any (real) arguments of the type of that constructor</span>
+  │    <span style="font-family:serif">(primarily because nattree does not have any (real) arguments) ... <span style="font-style:italic">(bullet 1)</span></span>
   │
-  ╰─ <span style="font-family:serif">concerning type <span style="font-family:monospace">∀ A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span>:</span>
-       <span style="font-family:serif">Type <span style="font-family:monospace">∀ A : Type, A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span></span>
-       <span style="font-family:serif">satisfies the positivity condition for <span style="font-family:monospace">list</span> because:</span>
+  ╰─ <span style="font-family:serif">concerning type <span style="font-family:monospace">∀ A → (nat → nattree A) → nattree A</span> of constructor <span style="font-family:monospace">cons</span>:</span>
+       <span style="font-family:serif">Type <span style="font-family:monospace">∀ A : Type, A → (nat → nattree A) → nattree A</span> of constructor <span style="font-family:monospace">cons</span></span>
+       <span style="font-family:serif">satisfies the positivity condition for <span style="font-family:monospace">nattree</span> because:</span>
        │
-       ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">Type</span> ... <span style="font-style:italic">(bullet 3)</span></span>
+       ├─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> occurs only strictly positively in <span style="font-family:monospace">Type</span> ... <span style="font-style:italic">(bullet 1)</span></span>
        │
-       ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">A</span> ... <span style="font-style:italic">(bullet 3)</span></span>
+       ├─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> occurs only strictly positively in <span style="font-family:monospace">A</span> ... <span style="font-style:italic">(bullet 1)</span></span>
        │
-       ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 4)</span></span>
+       ├─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> occurs only strictly positively in <span style="font-family:monospace">nat → nattree A</span> ... <span style="font-style:italic">(bullet 3+2)</span></span>
        │
-       ╰─ <span style="font-family:serif"><span style="font-family:monospace">list</span> satisfies the positivity condition for <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 1)</span></span>
+       ╰─ <span style="font-family:serif"><span style="font-family:monospace">nattree</span> satisfies the positivity condition for <span style="font-family:monospace">nattree A</span> ... <span style="font-style:italic">(bullet 1)</span></span>
 </pre>
 \end{rawhtml}
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index b27a4dc943..5c519e46e3 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 df0cd2b825..41ea0a5dcd 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-ltac.tex b/doc/refman/RefMan-ltac.tex
index 574591185c..5fb4585884 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -547,7 +547,7 @@ Yet another way of branching without backtracking is the following structure:
 $v_2$ which must be tactic values. The tactic value $v_1$ is applied in each
 subgoal independently and if it fails \emph{to progress} then $v_2$ is
 applied. {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ is equivalent to {\tt
-  first [} {\tt progress} {\tacexpr}$_1$ {\tt |} {\tt progress}
+  first [} {\tt progress} {\tacexpr}$_1$ {\tt |}
   {\tacexpr}$_2$ {\tt ]} (except that if it fails, it fails like
 $v_2$). Branching is left-associative.
 
@@ -561,7 +561,7 @@ The tactic
 is a generalization of the biased-branching tactics above. The
 expression {\tacexpr}$_1$ is evaluated to $v_1$, which is then applied
 to each subgoal independently. For each goal where $v_1$ succeeds at
-least once, {tacexpr}$_2$ is evaluated to $v_2$ which is then applied
+least once, {\tacexpr}$_2$ is evaluated to $v_2$ which is then applied
 collectively to the generated subgoals. The $v_2$ tactic can trigger
 backtracking points in $v_1$: where $v_1$ succeeds at least once, {\tt
   tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a2d45046b0..675c2bf174 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}}
diff --git a/doc/refman/index.html b/doc/refman/index.html
index 9b5250abcb..b937350e6e 100644
--- a/doc/refman/index.html
+++ b/doc/refman/index.html
@@ -11,4 +11,4 @@
   <FRAME SRC="menu.html">
 </FRAMESET>
 
-</HTML>
-\ No newline at end of file
+</HTML>