Add documentation for goal selectors.

doc/refman/RefMan-ltac.tex

@@ -25,6 +25,7 @@ \section{Syntax}
 \def\contexthyp{\textrm{\textsl{context\_hyp}}}
 \def\tacarg{\nterm{tacarg}}
 \def\cpattern{\nterm{cpattern}}
+\def\selector{\textrm{\textsl{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
@@ -104,6 +105,7 @@ \section{Syntax}
 & | & {\tt exactly\_once} {\tacexprpref}\\
 & | & {\tt timeout} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
 & | & {\tt time} \zeroone{\qstring} {\tacexprpref}\\
+& | & {\selector} {\tt :} {\tacexprpref}\\
 & | & {\tacexprinf} \\
 \\
 {\tacexprinf} & ::= &
@@ -203,7 +205,13 @@ \section{Syntax}
 & $|$ & {\integer} {\tt \,<\,} {\integer}\\
 & $|$ & {\integer} {\tt <=} {\integer}\\
 & $|$ & {\integer} {\tt \,>\,} {\integer}\\
-& $|$ & {\integer} {\tt >=} {\integer}
+& $|$ & {\integer} {\tt >=} {\integer}\\
+\\
+\selector & ::= &
+        [{\ident}]\\
+& $|$ & {\integer}\\
+& $|$ & \nelist{{\it (}{\integer} {\it |} {\integer} {\tt -} {\integer}{\it )}}
+          {\tt ,}
 \end{tabular}
 \end{centerframe}
 \caption{Syntax of the tactic language (continued)}
@@ -358,7 +366,36 @@ \section{Semantics}
 
 \end{Variants}
 
+\subsubsection[Goal selectors]{Goal selectors\label{ltac:selector}
+\tacindex{\tt :}\index{Tacticals!:@{\tt :}}}
+
+We can restrict the application of a tactic to a subset of
+the currently focused goals with:
+\begin{quote}
+{\selector} {\tt :} {\tacexpr}
+\end{quote}
+When selecting several goals, the tactic {\tacexpr} is applied globally to
+all selected goals.
+
+\begin{Variants}
+  \item{} [{\ident}] {\tt :} {\tacexpr}
+
+    In this variant, {\tacexpr} is applied locally to a goal
+    previously named by the user.
+
+  \item {\num} {\tt :} {\tacexpr}
+
+    In this variant, {\tacexpr} is applied locally to the
+    {\num}-th goal.
+
+  \item $n_1$-$m_1$, \dots, $n_k$-$m_k$ {\tt :} {\tacexpr}
+
+    In this variant, {\tacexpr} is applied globally to the subset
+    of goals described by the given ranges. You can write a single
+    $n$ as a shortcut for $n$-$n$ when specifying multiple ranges.
+\end{Variants}
 
+\ErrMsg \errindex{No such goal}
 
 \subsubsection[For loop]{For loop\tacindex{do}
 \index{Tacticals!do@{\tt do}}}

doc/refman/RefMan-tac.tex

@@ -42,14 +42,12 @@ \section{Invocation of tactics
 \index{tactic@{\tac}}}
 
 A tactic is applied as an ordinary command. It may be preceded by a
-goal selector: {\tt all} if the tactic is to be applied to every
-focused goal simultaneously, or a natural number $n$ if it is to be
-applied to the $n$-th goal. If no selector is specified, the default
+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}}
 \begin{tabular}{lcl}
-{\selector} & := & {\tt all} | {\num}\\
 {\commandtac} & ::= & {\selector} {\tt :} {\tac} {\tt .}\\
  & $|$ & {\tac} {\tt .}
 \end{tabular}
@@ -63,7 +61,9 @@ \section{Invocation of tactics
 the first goal. Using {\tt Set Default Goal Selector ``all''} will
 make is so that tactics are, by default, applied to every goal
 simultaneously. Then, to apply a tactic {\tt tac} to the first goal
-only, you can write {\tt 1:tac}.
+only, you can write {\tt 1:tac}. Although more selectors are available,
+only {\tt ``all''} or a single natural number are valid default
+goal selectors.
 
 \subsection[\tt Test Default Goal Selector.]
            {\tt Test Default Goal Selector.}

proofs/proof_global.ml

@@ -678,7 +678,7 @@ let print_goal_selector = function
 let parse_goal_selector = function
   | "all" -> Vernacexpr.SelectAll
   | i ->
-      let err_msg = "A selector must be \"all\" or a natural number." in
+      let err_msg = "The default selector must be \"all\" or a natural number." in
       begin try
               let i = int_of_string i in
               if i < 0 then Errors.error err_msg;