Documentation Declare Implicit Tactic, Print Canonical Projections, ... + légère restructuration autour de Proof with et Hint Rewrite + maj crédits

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9030 85f007b7-540e-0410-9357-904b9bb8a0f7

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}}