Merge branch 'v8.6'

2 files changed, 35 insertions, 24 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 1d89c17f47..9378529cbe 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -26,6 +26,7 @@ problems.
 \def\tacarg{\nterm{tacarg}}
 \def\cpattern{\nterm{cpattern}}
 \def\selector{\textrm{\textsl{selector}}}
+\def\toplevelselector{\textrm{\textsl{toplevel\_selector}}}
 
 The syntax of the tactic language is given Figures~\ref{ltac}
 and~\ref{ltac-aux}. See Chapter~\ref{BNF-syntax} for a description of
@@ -105,7 +106,7 @@ is understood as
 & | & {\tt exactly\_once} {\tacexprpref}\\
 & | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
 & | & {\tt time} \zeroone{\qstring} {\tacexprpref}\\
-& | & {\selector} {\tt :} {\tacexprpref}\\
+& | & {\tt only} {\selector} {\tt :} {\tacexprpref}\\
 & | & {\tacexprinf} \\
 \\
 {\tacexprinf} & ::= &
@@ -209,11 +210,14 @@ is understood as
 \\
 \selector & ::= &
         [{\ident}]\\
-& $|$ & {\tt all}\\
-& $|$ & {\tt par}\\
 & $|$ & {\integer}\\
 & $|$ & \nelist{{\it (}{\integer} {\it |} {\integer} {\tt -} {\integer}{\it )}}
-          {\tt ,}
+          {\tt ,}\\
+\\
+\toplevelselector & ::= &
+        \selector\\
+& $|$ & {\tt all}\\
+& $|$ & {\tt par}
 \end{tabular}
 \end{centerframe}
 \caption{Syntax of the tactic language (continued)}
@@ -374,7 +378,12 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$.
 We can restrict the application of a tactic to a subset of
 the currently focused goals with:
 \begin{quote}
-{\selector} {\tt :} {\tacexpr}
+  {\toplevelselector} {\tt :} {\tacexpr}
+\end{quote}
+We can also use selectors as a tactical, which allows to use them nested in
+a tactic expression, by using the keyword {\tt only}:
+\begin{quote}
+  {\tt only} {\selector} {\tt :} {\tacexpr}
 \end{quote}
 When selecting several goals, the tactic {\tacexpr} is applied globally to
 all selected goals.
@@ -396,11 +405,12 @@ all selected goals.
     of goals described by the given ranges. You can write a single
     $n$ as a shortcut for $n$-$n$ when specifying multiple ranges.
 
-  \item {\tt all: } {\tacexpr}
+  \item {\tt all:} {\tacexpr}
 
     In this variant, {\tacexpr} is applied to all focused goals.
+    {\tt all:} can only be used at the toplevel of a tactic expression.
 
-  \item {\tt par: } {\tacexpr}
+  \item {\tt par:} {\tacexpr}
 
     In this variant, {\tacexpr} is applied to all focused goals
     in parallel.  The number of workers can be controlled via the
@@ -409,7 +419,7 @@ all selected goals.
     on goals containing no existential variables and {\tacexpr} must
     either solve the goal completely or do nothing (i.e. it cannot make
     some progress).
-    {\tt par: } can only be used at the top level of a tactic expression.
+    {\tt par:} can only be used at the toplevel of a tactic expression.
 
 \end{Variants}
 
@@ -1279,7 +1289,7 @@ Prints a profile for all tactics that start with {\qstring}. Append a period (.)
 \begin{quote}
 {\tt Reset Ltac Profile}.
 \end{quote}
-Resets the profile, that is, deletes all accumulated information
+Resets the profile, that is, deletes all accumulated information.  Note that backtracking across a {\tt Reset Ltac Profile} will not restore the information.
 
 \begin{coq_eval}
 Reset Initial.
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 65b49893b0..d23a49bc67 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -46,13 +46,13 @@ goal selector (see Section \ref{ltac:selector}).
 If no selector is specified, the default
 selector (see Section \ref{default-selector}) is used.
 
-\newcommand{\selector}{\nterm{selector}}
+\newcommand{\toplevelselector}{\nterm{toplevel\_selector}}
 \begin{tabular}{lcl}
-{\commandtac} & ::= & {\selector} {\tt :} {\tac} {\tt .}\\
+{\commandtac} & ::= & {\toplevelselector} {\tt :} {\tac} {\tt .}\\
  & $|$ & {\tac} {\tt .}
 \end{tabular}
-\subsection[\tt Set Default Goal Selector ``\selector''.]
-           {\tt Set Default Goal Selector ``\selector''.
+\subsection[\tt Set Default Goal Selector ``\toplevelselector''.]
+           {\tt Set Default Goal Selector ``\toplevelselector''.
             \optindex{Default Goal Selector}
             \label{default-selector}}
 After using this command, the default selector -- used when no selector
@@ -4356,22 +4356,23 @@ vernacular command and printed using {\nobreak {\tt Print Firstorder
 
    Tries to solve the goal with {\tac} when no logical rule may apply.
 
- \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }
-   \tacindex{firstorder with}
-
-   Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search
-   environment.
-
  \item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ }
    \tacindex{firstorder using}
 
-   Adds lemmas in {\tt auto} hints bases {\qualid}$_1$ \dots\ {\qualid}$_n$
-   to the proof-search environment. If {\qualid}$_i$ refers to an inductive
-   type, it is the collection of its constructors which is added as hints.
+   Adds lemmas {\qualid}$_1$ \dots\ {\qualid}$_n$ to the proof-search
+   environment. If {\qualid}$_i$ refers to an inductive type, it is
+   the collection of its constructors which are added to the
+   proof-search environment.
 
-\item \texttt{firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+ \item {\tt firstorder with \ident$_1$ \dots\ \ident$_n$ }
+   \tacindex{firstorder with}
 
-  This combines the effects of the {\tt using} and {\tt with} options.
+   Adds lemmas from {\tt auto} hint bases \ident$_1$ \dots\ \ident$_n$
+   to the proof-search environment.
+
+\item \texttt{firstorder {\tac} using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+
+  This combines the effects of the different variants of \texttt{firstorder}.
 
 \end{Variants}