premiere passe V8

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

1 files changed, 40 insertions, 40 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index bce445e327..199a319ca5 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -2516,16 +2516,16 @@ Hint Extern 4 ~(?=?) => discriminate.
   with hints with a cost less than 4.
 
   One can even use some sub-patterns of the pattern in the tactic
-  script. A sub-pattern is a question mark followed by a number like
-  \texttt{?1} or \texttt{?2}. Here is an example:
+  script. A sub-pattern is a question mark followed by an ident, like
+  \texttt{?X1} or \texttt{?X2}. Here is an example:
 
 % Require EqDecide.
 \begin{coq_example*}
 Require Import List.
 \end{coq_example*}
 \begin{coq_example}
-Hint Extern 5   ({?1 = ?2} + {?1 <> ?2}) =>
- generalize ?1 ?2; decide equality : eqdec.
+Hint Extern 5   ({?X1 = ?X2} + {?X1 <> ?X2}) =>
+ generalize X1 X2; decide equality : eqdec.
 Goal 
 forall a b:list (nat * nat), {a = b} + {a <> b}.
 info auto with eqdec.
@@ -2660,34 +2660,34 @@ We describe in this section how to combine the tactics provided by the
 system to write synthetic proof scripts called {\em tacticals}. The
 tacticals are built using tactic operators we present below.
 
-\subsection{\tt Idtac}
-\tacindex{Idtac}
-\index{Tacticals!Idtac@{\tt Idtac}} The constant {\tt Idtac} is the
+\subsection{\tt idtac}
+\tacindex{idtac}
+\index{Tacticals!idtac@{\tt idtac}} The constant {\tt idtac} is the
 identity tactic: it leaves any goal unchanged.
 
-\subsection{\tt Fail}
-\tacindex{Fail}
-\index{Tacticals!Fail@{\tt Fail}}
+\subsection{\tt fail}
+\tacindex{fail}
+\index{Tacticals!fail@{\tt fail}}
 
-The tactic {\tt Fail} is the always-failing tactic: it does not solve
+The tactic {\tt fail} is the always-failing tactic: it does not solve
 any goal. It is useful for defining other tacticals.
 
-\subsection{\tt Do {\num} {\tac}}
-\tacindex{Do}
-\index{Tacticals!Do@{\tt Do}}
+\subsection{\tt do {\num} {\tac}}
+\tacindex{do}
+\index{Tacticals!do@{\tt do}}
 This tactic operator repeats {\num} times the tactic {\tac}. It fails
 when it is not possible to repeat {\num} times the tactic.
 
-\subsection{\tt \tac$_1$ {\tt Orelse} \tac$_2$}
-\tacindex{Orelse}
-\index{Tacticals!Orelse@{\tt Orelse}}
-The tactical \tac$_1$ {\tt Orelse} \tac$_2$ tries to apply \tac$_1$
+\subsection{\tt \tac$_1$ {\tt ||} \tac$_2$}
+\tacindex{||}
+\index{Tacticals!orelse@{\tt ||}}
+The tactical \tac$_1$ {\tt ||} \tac$_2$ tries to apply \tac$_1$
 and, in case of a failure, applies \tac$_2$. It associates to the
 left.
 
-\subsection{\tt Repeat {\tac}}
-\index[tactic]{Repeat@{\tt Repeat}}
-\index{Tacticals!Repeat@{\tt Repeat}}
+\subsection{\tt repeat {\tac}}
+\index[tactic]{repeat@{\tt repeat}}
+\index{Tacticals!repeat@{\tt repeat}}
 
 This tactic operator repeats {\tac} as long as it does not fail.
 
@@ -2711,15 +2711,15 @@ first applies \tac$_0$ and then
 applies \tac$_i$ to the i-th subgoal generated by \tac$_0$. It  fails if
 $n$ is not the exact number of remaining subgoals.
 
-\subsection{\tt Try {\tac}}
-\tacindex{Try}
-\index{Tacticals!Try@{\tt Try}}
+\subsection{\tt try {\tac}}
+\tacindex{try}
+\index{Tacticals!try@{\tt try}}
 This tactic operator applies tactic \tac, and catches the possible
 failure of \tac. It never fails.
 
-\subsection{\tt First [ \tac$_0$ | \dots\ | \tac$_n$ ]}
-\tacindex{First}
-\index{Tacticals!First@{\tt First}}
+\subsection{\tt first [ \tac$_0$ | \dots\ | \tac$_n$ ]}
+\tacindex{first}
+\index{Tacticals!first@{\tt first}}
 
 This tactic operator tries to apply the tactics \tac$_i$ with $i=0\ldots{}n$,
 starting from $i=0$, until one of them does not fail. It fails if all the
@@ -2729,9 +2729,9 @@ tactics fail.
 \item \errindex{No applicable tactic.}
 \end{ErrMsgs}
 
-\subsection{\tt Solve [ \tac$_0$ | \dots\ | \tac$_n$ ]}
-\tacindex{Solve}
-\index{Tacticals!First@{\tt Solve}}
+\subsection{\tt solve [ \tac$_0$ | \dots\ | \tac$_n$ ]}
+\tacindex{solve}
+\index{Tacticals!solve@{\tt solve}}
 
 This tactic operator tries to solve the current goal with the tactics \tac$_i$
 with $i=0\ldots{}n$, starting from $i=0$, until one of them solves. It fails if
@@ -2741,17 +2741,17 @@ no tactic can solve.
 \item \errindex{Cannot solve the goal.}
 \end{ErrMsgs}
 
-\subsection{\tt Info {\tac}}
-\tacindex{Info}
-\index{Tacticals!Info@{\tt Info}}
+\subsection{\tt info {\tac}}
+\tacindex{info}
+\index{Tacticals!info@{\tt info}}
 This is not really a tactical. For elementary tactics, this is
 equivalent to \tac. For complex tactic like \texttt{auto}, it displays
 the operations performed by the tactic.
 
-\subsection{\tt Abstract {\tac}}
-\tacindex{Abstract}
-\index{Tacticals!Abstract@{\tt Abstract}}
-From outside, typing \texttt{Abstract \tac} is the same that
+\subsection{\tt abstract {\tac}}
+\tacindex{abstract}
+\index{Tacticals!abstract@{\tt abstract}}
+From outside, typing \texttt{abstract \tac} is the same that
 typing \tac. Internally it saves an auxiliary lemma called 
 {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
 current goal and \textit{n} is chosen so that this is a fresh name.
@@ -2762,7 +2762,7 @@ the user can avoid the explosion at time of the \texttt{Save} command
 without having to cut ``by hand'' the proof in smaller lemmas.
 
 \begin{Variants}
-\item \texttt{Abstract {\tac} using {\ident}}.\\
+\item \texttt{abstract {\tac} using {\ident}}.\\
   Give explicitly the name of the auxiliary lemma.
 \end{Variants}
 
@@ -2802,7 +2802,7 @@ of mutual induction for objects in type {\term$_i$}.
 \SeeAlso \ref{Scheme-examples}
 
 
-\section{Generation of induction principles with {\tt functional Scheme}}
+\section{Generation of induction principles with {\tt Functional Scheme}}
 \label{FunScheme}
 \comindex{Functional Scheme}
 
@@ -2852,7 +2852,7 @@ Ltac ElimBoolRewrite b H1 H2 :=
 \end{coq_example}
 
 The tactics macros are synchronous with the \Coq\ section mechanism:
-a \texttt{Tactic Definition} is deleted from the current environment
+a tactic definition is deleted from the current environment
 when you close the section (see also \ref{Section}) 
 where it was defined. If you want that a
 tactic macro defined in a module is usable in the modules that