diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 28 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 63 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 6 |
3 files changed, 66 insertions, 31 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 b668239a6a..2da12c8d69 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 @@ -1491,10 +1491,10 @@ the local context. \tacindex{contradiction} This tactic applies to any goal. The {\tt contradiction} tactic -attempts to find in the current context (after all {\tt intros}) one -hypothesis that is equivalent to {\tt False}. It permits to prune -irrelevant cases. This tactic is a macro for the tactics sequence -{\tt intros; elimtype False; assumption}. +attempts to find in the current context (after all {\tt intros}) an +hypothesis that is equivalent to an empty inductive type (e.g. {\tt + False}), to the negation of a singleton inductive type (e.g. {\tt + True} or {\tt x=x}), or two contradictory hypotheses. \begin{ErrMsgs} \item \errindex{No such assumption} @@ -2289,6 +2289,12 @@ giving \texttt{injection {\term} as} (with an empty list of names). To obtain this behavior, the option {\tt Set Structural Injection} must be activated. This option is off by default. +By default, \texttt{injection} only creates new equalities between +terms whose type is in sort \texttt{Type} or \texttt{Set}, thus +implementing a special behavior for objects that are proofs +of a statement in \texttt{Prop}. This behavior can be turned off +by setting the option \texttt{Set Keep Proof Equalities}. +\optindex{Keep Proof Equalities} \subsection{\tt inversion \ident} \tacindex{inversion} @@ -2308,6 +2314,14 @@ latter is first introduced in the local context using stock the lemmas whenever the same instance needs to be inverted several times. See Section~\ref{Derive-Inversion}. +\Rem Part of the behavior of the \texttt{inversion} tactic is to generate +equalities between expressions that appeared in the hypothesis that is +being processed. By default, no equalities are generated if they relate +two proofs (i.e. equalities between terms whose type is in +sort \texttt{Prop}). This behavior can be turned off by using the option +\texttt{Set Keep Proof Equalities.} +\optindex{Keep Proof Equalities} + \begin{Variants} \item \texttt{inversion \num} @@ -3293,6 +3307,16 @@ reduced to \texttt{S t}. \end{Variants} +\begin{quote} +\optindex{Refolding Reduction} +{\tt Refolding Reduction} +\end{quote} + +This option (off by default) controls the use of the refolding strategy +of {\tt cbn} while doing reductions in unification, type inference and +tactic applications. It can result in expensive unifications, as +refolding currently uses a potentially exponential heuristic. + \subsection{\tt unfold \qualid} \tacindex{unfold} \label{unfold} @@ -4346,22 +4370,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} diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 10271ce0ca..9962ce9961 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -102,7 +102,7 @@ generator using for instance the command: This command generates a file \texttt{Makefile} that can be used to compile all the sources of the current project. It follows the -syntax described by the output of \texttt{\% coq\_makefile ----help}. +syntax described by the output of \texttt{\% coq\_makefile -{}-help}. Once the \texttt{Makefile} file has been generated a first time, it can be used by the \texttt{make} command to compile part or all of the project. Note that once it has been generated once, as soon as @@ -112,8 +112,8 @@ automatically regenerated by an invocation of \texttt{make}. The following command generates a minimal example of \texttt{\_CoqProject} file: \begin{quotation} -\texttt{\% \{ echo '-R .} \textit{MyFancyLib} \texttt{' ; find . -name - '*.v' -print \} > \_CoqProject} +\texttt{\% ( echo "-R .\ }\textit{MyFancyLib}\texttt{" ; find .\ -name + "*.v" -print ) > \_CoqProject} \end{quotation} when executed at the root of the directory containing the project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files |