passe sur les labels et les refs dans chapitres tactiques

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

10 files changed, 51 insertions, 55 deletions

diff --git a/doc/Cases.tex b/doc/Cases.tex
index 11e20d110..9fcd8430c 100644
--- a/doc/Cases.tex
+++ b/doc/Cases.tex
@@ -438,7 +438,7 @@ In all the previous examples the elimination predicate does not depend
 on the object(s) matched. But it may depend and the typical case 
 is when we write a proof by induction or a function that yields an
 object of dependent type. An example of proof using \texttt{Cases} in
-given in section \ref{Refine-example}
+given in section \ref{refine-example}
 
 For example, we can write 
 the function \texttt{buildlist} that given a natural number
@@ -493,7 +493,7 @@ elimination predicate ${\cal P}$ should be of the form:
 $[\vec{d_1}:\vec{D_1}][x_1:T_1]\ldots [\vec{d_n}:\vec{D_n}][x_n:T_n]Q.$
 
 The user can also use \texttt{Cases} in combination with the tactic
-\texttt{Refine} (see section \ref{Refine}) to build incomplete proofs
+\texttt{refine} (see section \ref{refine}) to build incomplete proofs
 beginning with a \texttt{Cases} construction.
 
 \asection{Pattern-matching on inductive objects involving local
diff --git a/doc/Correctness.tex b/doc/Correctness.tex
index 98c5c4568..b87fdae8a 100644
--- a/doc/Correctness.tex
+++ b/doc/Correctness.tex
@@ -58,7 +58,7 @@ where $P$ and $Q$ stand for the pre- and post-conditions of the
 program, $\vec{x}$ and $\vec{y}$ the variables used and modified by
 the program and $v$ its result.
 Then this partial proof is given to the tactic \texttt{Refine}
-(see~\ref{Refine}, page~\pageref{Refine}), which effect is to generate as many
+(see~\ref{refine}, page~\pageref{refine}), which effect is to generate as many
 subgoals as holes in the partial proof term.
 
 \medskip
diff --git a/doc/Polynom.tex b/doc/Polynom.tex
index d12781392..02c49577b 100644
--- a/doc/Polynom.tex
+++ b/doc/Polynom.tex
@@ -1,7 +1,7 @@
-\achapter{The \texttt{Ring} tactic}
+\achapter{The \texttt{ring} tactic}
 \aauthor{Patrick Loiseleur and Samuel Boutin}
-\label{Ring}
-\tacindex{Ring}
+\label{ring}
+\tacindex{ring}
 
 This chapter presents  the \texttt{Ring} tactic.
 
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex
index 6ac29e487..93b3d0f25 100644
--- a/doc/RefMan-gal.tex
+++ b/doc/RefMan-gal.tex
@@ -778,7 +778,7 @@ environment, provided that {\term} is well-typed.
     \texttt{Actually, it has type {\term$_3$}}.
 \end{ErrMsgs}
 
-\SeeAlso sections \ref{Opaque}, \ref{Transparent}, \ref{Unfold}
+\SeeAlso sections \ref{Opaque}, \ref{Transparent}, \ref{unfold}
 
 \subsubsection{\tt Local {\ident} := {\term}.}\comindex{Local}
 This command binds the value {\term} to the name {\ident} in the
@@ -797,7 +797,7 @@ definition is a kind of {\em macro}.
 \end{Variants}
 
 \SeeAlso \ref{Section} (section mechanism), \ref{Opaque},
-\ref{Transparent} (opaque/transparent constants), \ref{Unfold}
+\ref{Transparent} (opaque/transparent constants), \ref{unfold}
 
 % Let comme forme de Definition n'existe plus
 %
@@ -962,7 +962,7 @@ equivalent to \\ {\tt Inductive {\ident} : {\sort} :=
       Same as before but with parameters.
 \end{Variants}
 
-\SeeAlso sections \ref{Cic-inductive-definitions}, \ref{Elim}
+\SeeAlso sections \ref{Cic-inductive-definitions}, \ref{elim}
 
 \subsubsection{Mutually inductive types}
 \comindex{Mutual Inductive}\label{Mutual-Inductive}
@@ -1366,7 +1366,7 @@ It is a synonymous of \texttt{Theorem}
 \item {\tt Definition {\ident} : {\type}.} \\
 Allow to define a term of type {\type} using the proof editing mode. It
 behaves as {\tt Theorem} except the defined term will be transparent (see
-\ref{Transparent}, \ref{Unfold}). 
+\ref{Transparent}, \ref{unfold}). 
 \end{Variants}
 
 \subsubsection{{\tt Proof} {\tt .} \dots {\tt Qed} {\tt .}}
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 1a6aa2dab..757a0e2ce 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -541,7 +541,7 @@ provides a scope {\tt nat\_scope} gathering standard notations for
 common operations (+,*) and a decimal notation for numbers. That is he
 can write \texttt{3} for \texttt{(S (S (S O)))}. This also works on
 the left hand side of a \texttt{match} expression (see for example
-section \ref{Refine-example}). This scope is opened by default.
+section~\ref{refine-example}). This scope is opened by default.
 
 %Remove the redefinition of nat
 \begin{coq_eval}
diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index bc5b61fec..3adecde1d 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -22,7 +22,7 @@ generated by the tactics.
 To each subgoal is associated  a number of
 hypotheses we call the {\em \index*{local context}} of the goal.
 Initially, the local context is empty. It is enriched by the use of
-certain tactics (see mainly section \ref{Intro}).
+certain tactics (see mainly section~\ref{intro}).
 
 When a proof is achieved the message {\tt Proof completed} is
 displayed. One can then store this proof as a defined constant in the
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 199a319ca..92fbc42d8 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -120,7 +120,7 @@ convertible (see section \ref{conv-rules}).
 
 \subsection{\tt refine \term}
 \tacindex{refine}
-\label{Refine}
+\label{refine}
 \index{?@{\texttt{?}}}
 
 This tactic allows to give an exact proof but still with some
@@ -140,7 +140,7 @@ holes. The holes are noted ``\texttt{?}''.
 \end{ErrMsgs}
 
 This tactic is currently given as an experiment. An example of use is given
-in section~\ref{Refine-example}.
+in section~\ref{refine-example}.
 
 \section{Basics}
 \index{Typing rules}
@@ -339,7 +339,7 @@ instantiations of the premises of the type of {\term}.
   know that the conclusion of {\term} and the current goal are
   unifiable, you can help the {\tt apply} tactic by transforming your
   goal with the {\tt change} or {\tt pattern} tactics (see sections
-  \ref{Pattern}, \ref{Change}).
+  \ref{pattern}, \ref{change}).
 
 \item \errindex{Cannot refine to conclusions with meta-variables}
 
@@ -1787,7 +1787,7 @@ the instance with the tactic {\tt Inversion}.
   inverted the instance with the tactic \texttt{Dependent Inversion\_clear}.
 \end{Variants}
 
-\SeeAlso \ref{Inversion-examples} for examples
+\SeeAlso \ref{inversion-examples} for examples
 
 \subsection{\tt quote \ident}\tacindex{quote}
 \index{2-level approach}
@@ -1816,7 +1816,7 @@ datatype: see~\ref{quote-examples} for the full details.
 \label{Automatizing}
 
 \subsection{\tt auto}
-\tacindex{auto}
+\label{auto}\tacindex{auto}
 This tactic implements a Prolog-like resolution procedure to solve the
 current goal. It first tries to solve the goal using the {\tt
   assumption} tactic, then it reduces the goal to an atomic one using
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex
index deccfc336..8503630a5 100644
--- a/doc/RefMan-tacex.tex
+++ b/doc/RefMan-tacex.tex
@@ -43,8 +43,8 @@ Defined.
 
 % \texttt{Refine} is actually the only way for the user to do
 % a proof with the same structure as a {\tt Cases} definition. Actually,
-% the tactics \texttt{Case} (see \ref{Case}) and \texttt{Elim} (see
-% \ref{Elim}) only allow one step of elementary induction. 
+% the tactics \texttt{case} (see \ref{case}) and \texttt{Elim} (see
+% \ref{elim}) only allow one step of elementary induction. 
 
 % \begin{coq_example*}
 % Require Bool.
@@ -436,14 +436,14 @@ cases. Inversion tools can be classified in three groups:
 \begin{enumerate}
 \item tactics for inverting an instance without stocking the inversion
   lemma in the context; this includes the tactics
-  (\texttt{Dependent})  \texttt{Inversion} and
- (\texttt{Dependent}) \texttt{Inversion\_clear}.
+  (\texttt{dependent})  \texttt{inversion} and
+ (\texttt{dependent}) \texttt{inversion\_clear}.
 \item commands for generating and stocking in the context the inversion
   lemma corresponding to an instance; this includes \texttt{Derive}
   (\texttt{Dependent}) \texttt{Inversion} and \texttt{Derive}
   (\texttt{Dependent}) \texttt{Inversion\_clear}.
 \item tactics for inverting an instance using an already defined
-  inversion lemma; this includes the tactic \texttt{Inversion \ldots using}.
+  inversion lemma; this includes the tactic \texttt{inversion \ldots using}.
 \end{enumerate}
 
 As inversion proofs may be large in size, we recommend the user to
@@ -462,7 +462,7 @@ Reset Initial.
 
 \begin{coq_example*}
 Inductive Le : nat -> nat -> Set :=
-  | LeO : forall n:nat, Le 0%N n
+  | LeO : forall n:nat, Le 0 n
   | LeS : forall n m:nat, Le n m -> Le (S n) (S m).
 Variable P : nat -> nat -> Prop.
 Variable Q : forall n m:nat, Le n m -> Prop.
@@ -499,7 +499,7 @@ context.
 
 Sometimes it is
 interesting to have the equality \texttt{m=(S m0)} in the
-context to use it after. In that case we can use  \texttt{Inversion} that
+context to use it after. In that case we can use \texttt{inversion} that
 does not clear the equalities:
 
 \begin{coq_example*}
@@ -573,10 +573,10 @@ inversion H using leminv.
 Reset Initial.
 \end{coq_eval}
 
-\section{\tt AutoRewrite}
-\label{AutoRewrite-example}
+\section{\tt autorewrite}
+\label{autorewrite-example}
 
-Here are two examples of {\tt AutoRewrite} use. The first one ({\em Ackermann
+Here are two examples of {\tt autorewrite} use. The first one ({\em Ackermann
 function}) shows actually a quite basic use where there is no conditional
 rewriting. The second one ({\em Mac Carthy function}) involves conditional
 rewritings and shows how to deal with them using the optional tactic of the
@@ -599,7 +599,7 @@ Axiom Ack2 : forall n m:nat, Ack (S n) (S m) = Ack n (Ack (S n) m).
 \begin{coq_example}
 Hint Rewrite [ Ack0 Ack1 Ack2 ] in base0.
 Lemma ResAck0 : 
- Ack 3 2 = 29%N.
+ Ack 3 2 = 29.
 autorewrite [ base0 ] using try reflexivity.
 \end{coq_example}
 
@@ -619,17 +619,17 @@ Axiom g0 :
 Axiom
   g1 :
     forall n m:nat,
-      (n > 0)%N -> (m > 100)%N -> g n m = g (pred n) (m - 10).
+      (n > 0) -> (m > 100) -> g n m = g (pred n) (m - 10).
 Axiom
   g2 :
     forall n m:nat,
-      (n > 0)%N -> (m <= 100)%N -> g n m = g (S n) (m + 11).
+      (n > 0) -> (m <= 100) -> g n m = g (S n) (m + 11).
 \end{coq_example*}
 
 \begin{coq_example}
 Hint Rewrite [ g0 g1 g2 ] in base1 using omega.
 Lemma Resg0 : 
- g 1 110 = 100%N.
+ g 1 110 = 100.
 autorewrite [ base1 ] using reflexivity || simpl.
 \end{coq_example}
 
@@ -638,7 +638,7 @@ Abort.
 \end{coq_eval}
 
 \begin{coq_example}
-Lemma Resg1 : g 1 95 = 91%N.
+Lemma Resg1 : g 1 95 = 91.
 autorewrite [ base1 ] using reflexivity || simpl.
 \end{coq_example}
 
@@ -646,16 +646,16 @@ autorewrite [ base1 ] using reflexivity || simpl.
 Reset Initial.
 \end{coq_eval}
 
-\section{\tt Quote}
-\tacindex{Quote}
-\label{Quote-examples}
+\section{\tt quote}
+\tacindex{quote}
+\label{quote-examples}
 
-The tactic \texttt{Quote} allows to use Barendregt's so-called
+The tactic \texttt{quote} allows to use Barendregt's so-called
 2-level approach without writing any ML code. Suppose you have a
 language \texttt{L} of 
 'abstract terms' and a type \texttt{A} of 'concrete terms' 
 and a function \texttt{f : L -> A}. If \texttt{L} is a simple
-inductive datatype and \texttt{f} a simple fixpoint, \texttt{Quote f}
+inductive datatype and \texttt{f} a simple fixpoint, \texttt{quote f}
 will replace the head of current goal by a convertible term of the form 
 \texttt{(f t)}. \texttt{L} must have a constructor of type: \texttt{A
   -> L}. 
@@ -692,25 +692,21 @@ return the corresponding constructor (here \texttt{f\_const}) applied
 to the term. 
 
 \begin{ErrMsgs}
-\item \errindex{Quote: not a simple fixpoint} \\
-  Happens when \texttt{Quote} is not able to perform inversion properly.
+\item \errindex{quote: not a simple fixpoint} \\
+  Happens when \texttt{quote} is not able to perform inversion properly.
 \end{ErrMsgs}
 
 \subsection{Introducing variables map}
 
-The normal use of \texttt{Quote} is to make proofs by reflection: one
+The normal use of \texttt{quote} is to make proofs by reflection: one
 defines a function \texttt{simplify : formula -> formula} and proves a 
 theorem \texttt{simplify\_ok: (f:formula)(interp\_f (simplify f)) ->
   (interp\_f f)}. Then, one can simplify formulas by doing:
-
-\begin{quotation}
 \begin{verbatim}
-   Quote interp_f.
-   Apply simplify_ok.
-   Compute.
+   quote interp_f.
+   apply simplify_ok.
+   compute.
 \end{verbatim}
-\end{quotation}
-
 But there is a problem with leafs: in the example above one cannot
 write a function that implements, for example, the logical simplifications 
 $A \wedge A \ra A$ or $A \wedge \neg A \ra \texttt{False}$. This is
@@ -730,11 +726,11 @@ Inductive formula : Set :=
   | f_atom : index -> formula.
 \end{coq_example*}
 
-\texttt{index} is defined in module \texttt{Quote}. Equality on that
+\texttt{index} is defined in module \texttt{quote}. Equality on that
 type is decidable so we are able to simplify $A \wedge A$ into $A$ at
 the abstract level. 
 
-When there are variables, there are bindings, and \texttt{Quote}
+When there are variables, there are bindings, and \texttt{quote}
 provides also a type \texttt{(varmap A)} of bindings from
 \texttt{index} to any set \texttt{A}, and a function
 \texttt{varmap\_find} to search in such maps. The interpretation
@@ -752,7 +748,7 @@ Fixpoint interp_f (vm:
   end.
 \end{coq_example}
 
-\noindent\texttt{Quote} handles this second case properly:
+\noindent\texttt{quote} handles this second case properly:
 
 \begin{coq_example}
 Goal A /\ (B \/ A) /\ (A \/ ~ B).
@@ -765,8 +761,8 @@ convertible with the conclusion of current goal.
 \subsection{Combining variables and constants}
 
 One can have both variables and constants in abstracts terms; that is
-the case, for example, for the \texttt{Ring} tactic (chapter
-\ref{Ring}). Then one must provide to Quote a list of
+the case, for example, for the \texttt{ring} tactic (chapter
+\ref{ring}). Then one must provide to \texttt{quote} a list of
 \emph{constructors of constants}. For example, if the list is
 \texttt{[O S]} then closed natural numbers will be considered as
 constants and other terms as variables. 
@@ -812,7 +808,7 @@ is undecidable in general case, don't expect miracles from it!
 
 \SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml}
 
-\SeeAlso the tactic \texttt{Ring} (chapter \ref{Ring})
+\SeeAlso the tactic \texttt{ring} (chapter \ref{ring})
 
 
 %%% Local Variables: 
diff --git a/doc/RefMan-tus.tex b/doc/RefMan-tus.tex
index d296c0b47..8be5c9635 100755
--- a/doc/RefMan-tus.tex
+++ b/doc/RefMan-tus.tex
@@ -771,7 +771,7 @@ arguments for tactics is a union type including:
 \item well-typed terms, represented by a construction;
 \item a substitution for bound variables, like the
 substitution in the tactic \\$\texttt{Apply}\;t\;\texttt{with}\;x:=t_1\ldots
-x_n:=t_n$, (cf. Section \ref{Apply});
+x_n:=t_n$, (cf. Section~\ref{apply});
 \item a reduction expression, denoting the reduction strategy to be
 followed.
 \end{itemize}
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 229fb4524..7a5c5eca4 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -18,7 +18,7 @@
 \fi
 
 
-%\includeonly{RefMan-tac.v,RefMan-tacex.v}
+\includeonly{RefMan-tac.v,RefMan-tacex.v}
 
 \input{./version.tex}
 \input{./macros.tex}% extension .tex pour htmlgen