Report de la révision #12200 (bug #2125)

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

2 files changed, 45 insertions, 45 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 5b447f350..d5c8cf4ed 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -5,7 +5,7 @@
 This chapter gives a compact documentation of Ltac, the tactic
 language available in {\Coq}. We start by giving the syntax, and next,
 we present the informal semantics. If you want to know more regarding
-this language and especially about its fundations, you can refer
+this language and especially about its foundations, you can refer
 to~\cite{Del00}. Chapter~\ref{Tactics-examples} is devoted to giving
 examples of use of this language on small but also with non-trivial
 problems.
@@ -37,7 +37,7 @@ integer numbers, the authorized identificators and qualified names,
 Chapter~\ref{Tactics}. The syntax of {\cpattern} is the same as that
 of terms, but it is extended with pattern matching metavariables. In
 {\cpattern}, a pattern-matching metavariable is represented with the
-syntax {\tt ?id} where {\tt id} is a {\ident}. The notation {\tt \_}
+syntax {\tt ?id} where {\tt id} is an {\ident}. The notation {\tt \_}
 can also be used to denote metavariable whose instance is
 irrelevant. In the notation {\tt ?id}, the identifier allows us to
 keep instantiations and to make constraints whereas {\tt \_} shows
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 1eaeb64c3..d3d1ad918 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1939,10 +1939,10 @@ of type {\tt forall $x$:$T$, $P$} (dependent product), the behavior of
 {\tt intros $p$} is defined inductively over the structure of the
 introduction pattern $p$:
 \begin{itemize}
-\item introduction on \texttt{?} performs the introduction, and let {\Coq}
+\item introduction on \texttt{?} performs the introduction, and lets {\Coq}
   choose a fresh name for the variable;
 \item introduction on \texttt{?\ident} performs the introduction, and
-  let {\Coq} choose a fresh name for the variable based on {\ident};
+  lets {\Coq} choose a fresh name for the variable based on {\ident};
 \item introduction on \texttt{\ident} behaves as described in
   Section~\ref{intro};
 \item introduction over a disjunction of list of patterns {\tt
@@ -2045,7 +2045,7 @@ more concise subgoals.
 
 This applies double induction on the \num$_1^{th}$ and \num$_2^{th}$ {\it
 non dependent} premises of the goal. More generally, any combination of an
-{\ident} and an {\num} is valid.
+{\ident} and a {\num} is valid.
 
 \end{Variant}
 
@@ -2227,7 +2227,7 @@ details.
  (see Section~\ref{Tac-induction}), allows to give explicitly the
  induction principle and the values of dependent premises of the
  elimination scheme, including \emph{predicates} for mutual induction
- when \qualid is mutually recursive.
+ when {\qualid} is mutually recursive.
 
 \item {\tt functional induction (\qualid\ \term$_1$ \dots\ \term$_n$)
     using \term$_{m+1}$ with {\vref$_1$} := {\term$_{n+1}$} \dots\
@@ -2237,7 +2237,7 @@ details.
   (see Section~\ref{Tac-induction}).
 
 \item All previous variants can be extended by the usual \texttt{as
-    \intropattern} construction, similarly for example to
+    \intropattern} construction, similar for example to
   \texttt{induction} and \texttt{elim} (see Section~\ref{Tac-induction}).
     
 \end{Variants}
@@ -2296,7 +2296,7 @@ This happens if \term$_1$ does not occur in the goal.
   \textit{clause} (similarly to \ref{Conversion-tactics}). For
   instance:
   \begin{itemize}
-  \item \texttt{rewrite H in H1} will rewrites \texttt{H} in the hypothesis
+  \item \texttt{rewrite H in H1} will rewrite \texttt{H} in the hypothesis
     \texttt{H1} instead of the current goal.
   \item \texttt{rewrite H in H1 at 1, H2 at - 2 |- *} means \texttt{rewrite H; rewrite H in H1 at 1;
       rewrite H in H2 at - 2}. In particular a failure will happen if any of
@@ -2326,13 +2326,13 @@ This happens if \term$_1$ does not occur in the goal.
   Use {\tac} to completely solve the side-conditions arising from the
   rewrite.
 
-\item {\tt rewrite $\term_1$, \ldots, $term_n$}\\
+\item {\tt rewrite $\term_1$, \ldots, $\term_n$}\\
   Is equivalent to the $n$ successive tactics {\tt rewrite $\term_1$}
   up to {\tt rewrite $\term_n$}, each one working on the first subgoal
   generated by the previous one.
   Orientation {\tt ->} or {\tt <-} can be
   inserted before each term to rewrite. One unique \textit{clause}
-  can be added at the end after the keyword {\tt in}, it will 
+  can be added at the end after the keyword {\tt in}; it will 
   then affect all rewrite operations.
 
 \item In all forms of {\tt rewrite} described above, a term to rewrite
@@ -2386,18 +2386,20 @@ n}| assumption || symmetry; try assumption]}.
   as {\tt replace {\term$_1$} with {\term$_2$}} but applies {\tt \tac}
   to solve the generated subgoal {\tt \term$_2$=\term$_1$}.
 \item {\tt replace {\term}}\\ Replace {\term} with {\term'} using the
-  first assumption which type has the form {\tt \term=\term'} or {\tt
+  first assumption whose type has the form {\tt \term=\term'} or {\tt
     \term'=\term}
 \item {\tt replace -> {\term}}\\ Replace {\term} with {\term'} using the
-  first assumption which type has the form {\tt \term=\term'}
+  first assumption whose type has the form {\tt \term=\term'}
 \item {\tt replace <- {\term}}\\ Replace {\term} with {\term'} using the
-  first assumption which type has the form {\tt \term'=\term}
+  first assumption whose type has the form {\tt \term'=\term}
 \item {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} }\\
     {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} by \tac }\\ 
     {\tt replace {\term} \textit{clause}}\\ 
     {\tt replace -> {\term} \textit{clause}}\\ 
-    {\tt replace -> {\term} \textit{clause}}\\ 
-    Act as before but the replacements take place in \textit{clause}~\ref{Conversion-tactics} an not only in the conclusion of the goal.\\
+    {\tt replace <- {\term} \textit{clause}}\\ 
+    Act as before but the replacements take place in
+    \textit{clause}~(see Section~\ref{Conversion-tactics}) and not only
+    in the conclusion of the goal.\\
     The  \textit{clause} argument must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
 \end{Variants}
 
@@ -2411,7 +2413,7 @@ It is equivalent to {\tt apply refl\_equal}.
 
 \begin{ErrMsgs}
 \item \errindex{The conclusion is not a substitutive equation}
-\item \errindex{Impossible to unify \dots\ with ..}
+\item \errindex{Impossible to unify \dots\ with \dots.}
 \end{ErrMsgs}
 
 \subsection{\tt symmetry
@@ -2474,7 +2476,7 @@ accepted as regular setoids for {\tt rewrite} and {\tt
 \tacindex{stepr}
 \comindex{Declare Right Step}
 \begin{Variants}
-\item{\tt stepl {\term}{\sl n} by {\tac}}\\
+\item{\tt stepl {\term} by {\tac}}\\
 This applies {\tt stepl {\term}} then applies {\tac} to the second goal.
 
 \item{\tt stepr {\term}}\\
@@ -2903,12 +2905,12 @@ Abort.
   \texttt{dependent inversion\_clear} {\ident}\texttt{as} {\intropattern}
   
   This allows to name the hypotheses introduced in the context by
-  \texttt{dependent inversion\_clear} {\ident}
+  \texttt{dependent inversion\_clear} {\ident}.
 
 \item \tacindex{dependent inversion \dots\ with} \texttt{dependent
     inversion } {\ident} \texttt{ with } \term  
   
-  This variant allow to give the good generalization of the goal. It
+  This variant allows you to specify the generalization of the goal. It
   is useful when the system fails to generalize the goal automatically. If
   {\ident} has type $(I~\vec{t})$ and $I$ has type
   $forall (\vec{x}:\vec{T}), s$,   then \term~  must be of type
@@ -2925,7 +2927,7 @@ Abort.
 \item \tacindex{dependent inversion\_clear \dots\ with}
   \texttt{dependent inversion\_clear } {\ident} \texttt{ with } \term 
   
-  Like \texttt{dependent inversion \dots\ with} but clears \ident from
+  Like \texttt{dependent inversion \dots\ with} but clears {\ident} from
   the local context.
 
 \item \tacindex{dependent inversion\_clear \dots\ as \dots\ with}
@@ -2939,7 +2941,7 @@ Abort.
   
   It is a very primitive inversion tactic that derives all the necessary
   equalities  but it does not simplify the  constraints as
-  \texttt{inversion} do.
+  \texttt{inversion} does.
 
 \item \tacindex{simple inversion \dots\ as} \texttt{simple inversion}
   {\ident} \texttt{as} {\intropattern} 
@@ -2959,7 +2961,7 @@ Abort.
   {\ident} \texttt{using} \ident$'$ \texttt{in} \ident$_1$\dots\ \ident$_n$
   
   This tactic behaves as generalizing \ident$_1$\dots\ \ident$_n$,
-  then doing \texttt{inversion}{\ident}\texttt{using} \ident$'$.
+  then doing \texttt{inversion} {\ident} \texttt{using} \ident$'$.
 
 \end{Variants}
 
@@ -3012,7 +3014,7 @@ which performs inversion on hypothesis \ident\ of the form
 defined using \texttt{Function} (see Section~\ref{Function}).
 
 \begin{ErrMsgs}
-\item \errindex{Hypothesis \ident must contain at least one Function}
+\item \errindex{Hypothesis {\ident} must contain at least one Function}
 \item \errindex{Cannot find inversion information for hypothesis \ident}
   This error may be raised when  some inversion lemma failed to be
   generated by Function.
@@ -3027,11 +3029,11 @@ defined using \texttt{Function} (see Section~\ref{Function}).
 \item {\tt functional inversion \ident\ \qualid}\\
   {\tt functional inversion \num\ \qualid}
 
-  In case the hypothesis \ident (or \num) has a type of the form
-  \texttt{\qualid$_1$\ \term$_1$\dots\term$_n$\ =\qualid$_2$\
+  In case the hypothesis {\ident} (or {\num}) has a type of the form
+  \texttt{\qualid$_1$\ \term$_1$\dots\term$_n$\ =\ \qualid$_2$\
     \term$_{n+1}$\dots\term$_{n+m}$} where \qualid$_1$ and \qualid$_2$
   are valid candidates to functional inversion, this variant allows to
-  chose which must be inverted.
+  choose which must be inverted.
 \end{Variants}
 
 
@@ -3042,7 +3044,7 @@ defined using \texttt{Function} (see Section~\ref{Function}).
 
 This kind of inversion has nothing to do with the tactic
 \texttt{inversion} above. This tactic does \texttt{change (\ident\
-  t)}, where \texttt{t} is a term build in order to ensure the
+  t)}, where \texttt{t} is a term built in order to ensure the
 convertibility. In other words, it does inversion of the function
 \ident. This function must be a fixpoint on a simple recursive
 datatype: see~\ref{quote-examples} for the full details.
@@ -3054,7 +3056,7 @@ datatype: see~\ref{quote-examples} for the full details.
 
 \begin{Variants}
 \item \texttt{quote {\ident} [ \ident$_1$ \dots \ident$_n$ ]}\\
-  All terms that are build only with \ident$_1$ \dots \ident$_n$ will be
+  All terms that are built only with \ident$_1$ \dots \ident$_n$ will be
   considered by \texttt{quote} as constants rather than variables.
 \end{Variants}
 
@@ -3069,7 +3071,7 @@ In order to ease the proving process, when the {\tt Classical} module is loaded.
 
 The tactics \texttt{classical\_left} and \texttt{classical\_right} are the analog of the \texttt{left} and \texttt{right} but using classical logic. They can only be used for disjunctions.
 Use  \texttt{classical\_left} to prove the left part of the disjunction with the assumption that the negation of right part holds. 
-Use \texttt{classical\_left} to prove the right part of the disjunction with the assumption that the negation of left part holds. 
+Use \texttt{classical\_right} to prove the right part of the disjunction with the assumption that the negation of left part holds. 
 
 \section{Automatizing
 \label{Automatizing}}
@@ -3117,7 +3119,7 @@ hints of the database named {\tt core}.
 \item {\tt trivial}\tacindex{trivial}
 
   This tactic is a restriction of {\tt auto} that is not recursive and 
-  tries only hints which cost is 0. Typically it solves trivial
+  tries only hints which cost 0. Typically it solves trivial
   equalities like $X=X$.
 
 \item \texttt{trivial with \ident$_1$ \dots\ \ident$_n$}
@@ -3126,7 +3128,7 @@ hints of the database named {\tt core}.
 
 \end{Variants}
 
-\Rem {\tt auto} either solves completely the goal or else leave it
+\Rem {\tt auto} either solves completely the goal or else leaves it
 intact. \texttt{auto} and \texttt{trivial} never fail.
 
 \SeeAlso Section~\ref{Hints-databases}
@@ -3249,8 +3251,8 @@ and then uses {\tt auto} which completes the proof.
 
 Originally due to C{\'e}sar~Mu{\~n}oz, these tactics ({\tt tauto} and {\tt intuition})
 have been completely re-engineered by David~Delahaye using mainly the tactic
-language (see Chapter~\ref{TacticLanguage}). The code is now quite shorter and
-a significant increase in performances has been noticed. The general behavior
+language (see Chapter~\ref{TacticLanguage}). The code is now much shorter and
+a significant increase in performance has been noticed. The general behavior
 with respect to dependent types, unfolding and introductions has
 slightly changed to get clearer semantics. This may lead to some
 incompatibilities.
@@ -3484,7 +3486,7 @@ congruence.
     tactic to successfully solve the goal. Those additional arguments
     can be given to {\tt congruence} by filling in the holes in the
     terms given in the error message, using the {\tt with} variant
-    described below.
+    described above.
 \end{ErrMsgs}
 
 \subsection{\tt omega
@@ -3616,7 +3618,7 @@ command.
 \begin{Variant}
 \item {\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}\\
 Performs, in the same way, all the rewritings of the bases {\tt \ident$_1$ $...$
-$ident_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
+\ident$_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
 
 \item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}}
 
@@ -3709,11 +3711,11 @@ where {\sl hint\_definition} is one of the following expressions:
   type can be reduced to a type starting with a product, the tactic {\tt
     apply {\term}} is also stored in the hints list.
   
-  If the inferred type of \term\ does contain a dependent
+  If the inferred type of \term\ contains a dependent
   quantification on a predicate, it is added to the hint list of {\tt
     eapply} instead of the hint list of {\tt apply}. In this case, a
   warning is printed since the hint is only used by the tactic {\tt
-    eauto} (see \ref{eauto}). A typical example of hint that is used
+    eauto} (see \ref{eauto}). A typical example of a hint that is used
   only by \texttt{eauto} is a transitivity lemma.
 
   \begin{ErrMsgs}
@@ -3742,12 +3744,12 @@ where {\sl hint\_definition} is one of the following expressions:
 \comindex{Hint Immediate}
   
   This command adds {\tt apply {\term}; trivial} to the hint list
-  associated with the head symbol of the type of \ident in the given
+  associated with the head symbol of the type of {\ident} in the given
   database. This tactic will fail if all the subgoals generated by
   {\tt apply {\term}} are not solved immediately by the {\tt trivial}
-  tactic which only tries tactics with cost $0$.
+  tactic (which only tries tactics with cost $0$).
   
-  This command is useful for theorems such that the symmetry of equality
+  This command is useful for theorems such as the symmetry of equality
   or $n+1=m+1 \to n=m$ that we may like to introduce with a
   limited use in order to avoid useless proof-search.
   
@@ -3842,7 +3844,7 @@ Hint Extern 4 ~(?=?) => discriminate.
 \end{quotation}
 
   Now, when the head of the goal is a disequality, \texttt{auto} will
-  try \texttt{discriminate} if it does not succeed to solve the goal
+  try \texttt{discriminate} if it does not manage to solve the goal
   with hints with a cost less than 4.
   
   One can even use some sub-patterns of the pattern in the tactic
@@ -3873,7 +3875,7 @@ the tactic.
 \begin{Variants}
 \item \texttt{Hint} \textsl{hint\_definition} 
   
-  No database name is given : the hint is registered in the {\tt core} 
+  No database name is given: the hint is registered in the {\tt core} 
     database. 
 
 \item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:}
@@ -3978,7 +3980,7 @@ every moment.
 \item {\tt  Print Hint {\ident} }
 
  This command displays only tactics associated with \ident\ in the
- hints list. This is independent of the goal being edited, to this
+ hints list. This is independent of the goal being edited, so this
  command will not fail if no goal is being edited.
 
 \item {\tt Print Hint *}
@@ -4125,8 +4127,6 @@ general principle of mutual induction for objects in type {\term$_i$}.
 
 \end{Variants}
 
-\SeeAlso \ref{Scheme-examples}
-
 \SeeAlso Section~\ref{Scheme-examples}
 
 \subsection{Automatic declaration of schemes}