diff options
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 12 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 12 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 17 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 118 |
5 files changed, 108 insertions, 57 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 73fb391ddb..37660aa3a7 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1118,6 +1118,18 @@ the declaration \SeeAlso more examples in user contribution \texttt{category} (\texttt{Rocq/ALGEBRA}). +\subsubsection{Print Canonical Projections. +\comindex{Print Canonical Projections}} + +This displays the list of global names that are components of some +canonical structure. For each of them, the canonical structure of +which it is a projection is indicated. For instance, the above example +gives the following output: + +\begin{coq_example} +Print Canonical Projections. +\end{coq_example} + \subsection{Implicit types of variables} It is possible to bind variable names to a given type (e.g. in a diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 7af3f64156..0fd6f64d8f 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -267,6 +267,12 @@ applied and $v_i$ is applied to the $i$-th generated subgoal by the application of $v_0$, for $=1,...,n$. It fails if the application of $v_0$ does not generate exactly $n$ subgoals. +\variant If no tactic is given for the $i$-th generated subgoal, it +behaves as if the tactic {\tt idtac} were given. For instance, {\tt +split ; [ | auto ]} is a shortcut for +{\tt split ; [ idtac | auto ]}. + + \subsubsection{For loop} \tacindex{do} \index{Tacticals!do@{\tt do}} diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index add22103c8..27a5a6c88b 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -556,19 +556,19 @@ unresolved implicit has been implemented by Hugo Herbelin. Laurent Théry's contribution on strings and Pierre Letouzey and Jean-Christophe Filliâtre's contribution on finite maps have been integrated to the {\Coq} standard library. Pierre Letouzey developed a -library about finite sets ``à la Objective Caml'' and extended the -lists library. Pierre Letouzey's contribution on rational numbers -has been integrated too. +library about finite sets ``à la Objective Caml''. With Jean-Marc +Notin, he extended the library on lists. Pierre Letouzey's +contribution on rational numbers has been integrated and extended.. Pierre Corbineau extended his tactic for solving first-order statements. He wrote a reflection-based intuitionistic tautology solver. -Jean-Marc Notin took care of {\textsf{coqdoc}} and of the general -maintenance of the system. +Jean-Marc Notin significantly contributed to the general maintenance +of the system. He also took care of {\textsf{coqdoc}}. \begin{flushright} -Palaiseau, Apr. 2006\\ +Palaiseau, July 2006\\ Hugo Herbelin \end{flushright} diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 7565612d14..ddfce775dd 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -163,28 +163,21 @@ as a {\tt Theorem}, the name {\ident} is known at all section levels: current section. \end{Variants} -\subsection{\tt Proof {\term}.}\comindex{Proof} +\subsection{\tt Proof {\term}.} +\comindex{Proof} +\label{BeginProof} This command applies in proof editing mode. It is equivalent to {\tt exact {\term}; Save.} That is, you have to give the full proof in one gulp, as a proof term (see section \ref{exact}). -\begin{Variants} - -\item{\tt Proof.} +\variant {\tt Proof.} Is a noop which is useful to delimit the sequence of tactic commands which start a proof, after a {\tt Theorem} command. It is a good practice to use {\tt Proof.} as an opening parenthesis, closed in the script with a closing {\tt Qed.} -\item{\tt Proof with {\tac}.} - - This command may be used to start a proof. It defines a default - tactic to be used each time a tactic command is ended by - ``\verb#...#''. In this case the tactic command typed by the user is - equivalent to \emph{command};{\tac}. - -\end{Variants} +\SeeAlso {\tt Proof with {\tac}.} in section~\ref{ProofWith}. \subsection{\tt Abort.} \comindex{Abort} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index ae3d8fe043..d42969e1ac 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1567,7 +1567,7 @@ This happens if \term$_1$ does not occur in the goal. \item {\tt rewrite {\term} in \textit{clause}} \tacindex{rewrite \dots\ in}\\ Analogous to {\tt rewrite {\term}} but rewriting is done following - \textit{clause} (similarly to \ref{Conversion-tactic}). For instance: + \textit{clause} (similarly to \ref{Conversion-tactics}). For instance: \texttt{rewrite H in H1,H2 |- *} means \texttt{rewrite H in H1; rewrite H in H2; rewrite H} and \texttt{rewrite H in * |-} will do \texttt{try rewrite H in H$_i$} for all hypothesis \texttt{H$_i$ <> @@ -2801,50 +2801,17 @@ $ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step. \end{Variant} -\subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident -\comindex{Hint Rewrite}} - -This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$} -(their types must be equalities) in the rewriting base {\tt \ident} -with the default orientation (left to right). Notice that the -rewriting bases are distinct from the {\tt auto} hint bases and that -{\tt auto} does not take them into account. - -This command is synchronous with the section mechanism (see \ref{Section}): -when closing a section, all aliases created by \texttt{Hint Rewrite} in that -section are lost. Conversely, when loading a module, all \texttt{Hint Rewrite} -declarations at the global level of that module are loaded. - -\begin{Variants} -\item {\tt Hint Rewrite -> \term$_1$ \dots \term$_n$ : \ident}\\ -This is strictly equivalent to the command above (we only make explicit the -orientation which otherwise defaults to {\tt ->}). - -\item {\tt Hint Rewrite <- \term$_1$ \dots \term$_n$ : \ident}\\ -Adds the rewriting rules {\tt \term$_1$ \dots \term$_n$} with a right-to-left -orientation in the base {\tt \ident}. +\SeeAlso section \ref{HintRewrite} for feeding the database of lemmas used by {\tt autorewrite}. -\item {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}\\ -When the rewriting rules {\tt \term$_1$ \dots \term$_n$} in {\tt \ident} will -be used, the tactic {\tt \tac} will be applied to the generated subgoals, the -main subgoal excluded. - -%% \item -%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in \ident}\\ -%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using {\tac}}\\ -%% These are deprecated syntactic variants for -%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident} and -%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}. - -\end{Variants} - -\SeeAlso \ref{autorewrite-example} for examples showing the use of +\SeeAlso section \ref{autorewrite-example} for examples showing the use of this tactic. % En attente d'un moyen de valoriser les fichiers de demos %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v} -\section{The hints databases for {\tt auto} and {\tt eauto} +\section{Controlling automation} + +\subsection{The hints databases for {\tt auto} and {\tt eauto} \index{Hints databases} \label{Hints-databases} \comindex{Hint}} @@ -3134,6 +3101,43 @@ every moment. \end{Variants} +\subsection{\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident +\label{HintRewrite} +\comindex{Hint Rewrite}} + +This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$} +(their types must be equalities) in the rewriting base {\tt \ident} +with the default orientation (left to right). Notice that the +rewriting bases are distinct from the {\tt auto} hint bases and that +{\tt auto} does not take them into account. + +This command is synchronous with the section mechanism (see \ref{Section}): +when closing a section, all aliases created by \texttt{Hint Rewrite} in that +section are lost. Conversely, when loading a module, all \texttt{Hint Rewrite} +declarations at the global level of that module are loaded. + +\begin{Variants} +\item {\tt Hint Rewrite -> \term$_1$ \dots \term$_n$ : \ident}\\ +This is strictly equivalent to the command above (we only make explicit the +orientation which otherwise defaults to {\tt ->}). + +\item {\tt Hint Rewrite <- \term$_1$ \dots \term$_n$ : \ident}\\ +Adds the rewriting rules {\tt \term$_1$ \dots \term$_n$} with a right-to-left +orientation in the base {\tt \ident}. + +\item {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}\\ +When the rewriting rules {\tt \term$_1$ \dots \term$_n$} in {\tt \ident} will +be used, the tactic {\tt \tac} will be applied to the generated subgoals, the +main subgoal excluded. + +%% \item +%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in \ident}\\ +%% {\tt Hint Rewrite [ \term$_1$ \dots \term$_n$ ] in {\ident} using {\tac}}\\ +%% These are deprecated syntactic variants for +%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ : \ident} and +%% {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}. + +\end{Variants} \subsection{Hints and sections \label{Hint-and-Section}} @@ -3144,6 +3148,42 @@ defined inside a section (and not defined with option {\tt Local}) become available when the module {\tt A} is imported (using e.g. \texttt{Require Import A.}). +\subsection{Setting implicit automation tactics} + +\subsubsection{\tt Proof with {\tac}.} +\label{ProofWith} +\comindex{Proof with} + + This command may be used to start a proof. It defines a default + tactic to be used each time a tactic command {\tac$_1$} is ended by + ``\verb#...#''. In this case the tactic command typed by the user is + equivalent to \tac$_1$;{\tac}. + +\SeeAlso {\tt Proof.} in section~\ref{BeginProof}. + +\subsubsection{\tt Declare Implicit Tactic {\tac}.} +\comindex{Declare Implicit Tactic} + +This command declares a tactic to be used to solve implicit arguments +that {\Coq} does not know how to solve by unification. It is used +every time the term argument of a tactic has one of its holes not +fully resolved. + +Here is an example: + +\begin{coq_example} +Parameter quo : nat -> forall n:nat, n<>0 -> nat. +Notation "x // y" := (quo x y _) (at level 40). + +Declare Implicit Tactic assumption. +Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. +intros. +exists (n // m). +\end{coq_example} + +The tactic {\tt exists (n // m)} did not fail. The hole was solved by +{\tt assumption} so that it behaved as {\tt exists (quo n m H)}. + \section{Generation of induction principles with {\tt Scheme} \label{Scheme} \comindex{Scheme}} |