diff options
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 39 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 10 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 2 |
3 files changed, 44 insertions, 7 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index ffcb37134..722249191 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -25,6 +25,7 @@ problems. \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 @@ is understood as & | & {\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 @@ is understood as & $|$ & {\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 @@ for $=1,...,n$. It fails if the number of focused goals is not exactly $n$. \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}}} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 54450fe7d..527226f68 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -42,14 +42,12 @@ language will be described in Chapter~\ref{TacticLanguage}. \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 @@ initial value is $1$, hence the tactics are, by default, applied to 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.} diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index be353b10a..61fe34750 100644 --- a/proofs/proof_global.ml +++ b/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; |