Fixed some typos in the reference manual.

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

5 files changed, 30 insertions, 29 deletions

diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 9e74463e1..eb22d4109 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -50,8 +50,8 @@ one monolithic file or one file per \Coq\ library.
       \qualid$_1$ \dots\ \qualid$_n$. ~\par
   Recursive extraction of all the globals (or modules) \qualid$_1$ \dots\
   \qualid$_n$ and all their dependencies in one monolithic file {\em file}.
-  Global and local identifiers are renamed according to the choosen ML
-  language to fullfill its syntactic conventions, keeping original
+  Global and local identifiers are renamed according to the chosen ML
+  language to fulfill its syntactic conventions, keeping original
   names as much as possible.
   
 \item {\tt Extraction Library} \ident. ~\par 
@@ -115,7 +115,7 @@ All these optimizations are controled by the following \Coq\ options:
 {\tt Unset Extraction Optimize.}
 
 Default is Set. This control all optimizations made on the ML terms 
-(mostly reduction of dummy beta/iota redexes, but also simplications on 
+(mostly reduction of dummy beta/iota redexes, but also simplifications on
 Cases, etc). Put this option to Unset if you want a ML term as close as 
 possible to the Coq term.
 
@@ -158,7 +158,7 @@ Puts the table recording the custom inlinings back to empty.
 
 \paragraph{Inlining and printing of a constant declaration.}
 
-A user can explicitely asks a constant to be extracted by two means: 
+A user can explicitly ask for a constant to be extracted by two means:
 \begin{itemize}
 \item by mentioning it on the extraction command line
 \item by extracting the whole \Coq\ module of this constant.
@@ -169,11 +169,11 @@ But this same constant may or may not be inlined in the following
 terms, depending on the automatic/custom inlining mechanism.  
 
 
-For the constants non-explicitely required but needed for dependancy
+For the constants non-explicitly required but needed for dependency
 reasons, there are two cases: 
 \begin{itemize}
-\item If an inlining decision is taken, wether automatically or not, 
-all occurences of this constant are replaced by its extracted body, and
+\item If an inlining decision is taken, whether automatically or not,
+all occurrences of this constant are replaced by its extracted body, and
 this constant is not declared in the generated file.
 \item If no inlining decision is taken, the constant is normally
   declared in the produced file. 
@@ -184,7 +184,7 @@ this constant is not declared in the generated file.
 Extraction will fail if it encounters an informative
 axiom not realized (see Section~\ref{extraction:axioms}). 
 A warning will be issued if it encounters an logical axiom, to remind 
-user that inconsistant logical axioms may lead to incorrect or 
+user that inconsistent logical axioms may lead to incorrect or
 non-terminating extracted terms. 
 
 It is possible to assume some axioms while developing a proof. Since
@@ -207,12 +207,12 @@ what ML term corresponds to a given axiom.
 Note that the {\tt Extract Inlined Constant} command is sugar
 for an {\tt Extract Constant} followed by a {\tt Extraction Inline}. 
 Hence a {\tt Reset Extraction Inline} will have an effect on the
-realized and inlined xaxiom. 
+realized and inlined axiom.
 
-Of course, it is the responsability of the user to ensure that the ML
+Of course, it is the responsibility of the user to ensure that the ML
 terms given to realize the axioms do have the expected types.  In
 fact, the strings containing realizing code are just copied in the
-extracted files. The extraction recognize whether the realized axiom
+extracted files. The extraction recognizes whether the realized axiom
 should become a ML type constant or a ML object declaration.
 
 \Example
@@ -243,12 +243,12 @@ Realizing an axiom via {\tt Extract Constant} is only useful in the
 case of an informative axiom (of sort Type or Set). A logical axiom
 have no computational content and hence will not appears in extracted
 terms. But a warning is nonetheless issued if extraction encounters a
-logical axiom. This warning reminds user that inconsistant logical
+logical axiom. This warning reminds user that inconsistent logical
 axioms may lead to incorrect or non-terminating extracted terms.
 
 If an informative axiom has not been realized before an extraction, a
 warning is also issued and the definition of the axiom is filled with
-an exception labelled {\tt AXIOM TO BE REALIZED}. The user must then
+an exception labeled {\tt AXIOM TO BE REALIZED}. The user must then
 search these exceptions inside the extracted file and replace them by
 real code.
 
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 5a3c91404..cf4774285 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -320,7 +320,7 @@ This tool can be used for several purposes. One is to check that a
 compiled library provided by a third-party has not been forged and
 that loading it cannot introduce inconsistencies.\footnote{Ill-formed
   non-logical information might for instance bind {\tt
-    Coq.Init.Logic.True} to short name {\tt False}, so apprently {\tt
+    Coq.Init.Logic.True} to short name {\tt False}, so apparently {\tt
     False} is inhabited, but using fully qualified names, {\tt
     Coq.Init.Logic.False} will always refer to the absurd proposition,
   what we guarantee is that there is no proof of this latter
@@ -341,7 +341,7 @@ same meaning as for {\tt coqtop}. Extra options are:
 \item[{\tt -admit} $module$] \
 
   Do not check $module$ and any of its dependencies, unless
-  explicitely required.
+  explicitly required.
 \item[{\tt -o}]\ 
 
   At exit, print a summary about the context. List the names of all
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 501f9b0b1..276c4c47a 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -161,7 +161,7 @@ Reset Initial.
    \item The body of {\ident$_i$} uses an incorrect elimination for
      {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}).
    \item The type of the projections {\ident$_i$} depends on previous
-   projections which themselves couldn't be defined.
+   projections which themselves could not be defined.
    \end{enumerate}  
 \end{Warnings}     
 
@@ -763,7 +763,8 @@ defined:
 
 %Complete!!
 The way this recursive function is defined is the subject of several
-papers by Yves Bertot and Antonia Balaa on one hand and  Gilles Barthe, Julien Forest, David Pichardie and Vlad Rusu on the other hand.
+papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles Barthe,
+Julien Forest, David Pichardie, and Vlad Rusu on the other hand.
 
 %Exemples ok ici
 
@@ -1097,7 +1098,7 @@ a-priori and a-posteriori.
 
 \subsubsection{Implicit Argument Binders}
 
-In the first setting, one wants to explicitely give the implicit
+In the first setting, one wants to explicitly give the implicit
 arguments of a constant as part of its definition. To do this, one has
 to surround the bindings of implicit arguments by curly braces:
 \begin{coq_eval}
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index ec7c9c0b1..8330a434b 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -630,7 +630,7 @@ generalize_eqs H.
 
 The index {\tt S n} gets abstracted by a variable here, but a
 corresponding equality is added under the abstract instance so that no
-information is actually lost. The goal is now almost ammenable to do induction
+information is actually lost. The goal is now almost amenable to do induction
 or case analysis. One should indeed first move {\tt n} into the goal to
 strengthen it before doing induction, or {\tt n} will be fixed in
 the inductive hypotheses (this does not matter for case analysis). 
@@ -665,7 +665,7 @@ substitute the equalities back into the instance to get the right
 assumptions. Sometimes injection of constructors will also be needed to
 recover the needed equalities. Also, some subgoals should be directly
 solved because of inconsistent contexts arising from the constraints on 
- indices. The nice thing is that we can make a tactic based on
+indexes. The nice thing is that we can make a tactic based on
 discriminate, injection and variants of substitution to automatically 
 do such simplifications (which may involve the K axiom). 
 This is what the {\tt simplify\_dep\_elim} tactic from
@@ -683,7 +683,7 @@ induction p ; simplify_dep_elim.
 
 The higher-order tactic {\tt do\_depind} defined in {\tt
   Coq.Program.Equality} takes a tactic and combines the
-building blocks we've seen with it: generalizing by equalities 
+building blocks we have seen with it: generalizing by equalities
 calling the given tactic with the
 generalized induction hypothesis as argument and cleaning the subgoals
 with respect to equalities. Its most important instantiations are
@@ -803,7 +803,7 @@ With this proper separation of the index from the instance and the right
 induction loading (putting {\tt G} and {\tt D} after the inducted-on
 hypothesis), the proof will go through, but it is a very tedious
 process. One is also forced to make a wrapper lemma to get back the
-more natural statement. The \depind tactic aleviates this trouble by
+more natural statement. The \depind tactic alleviates this trouble by
 doing all of this plumbing of generalizing and substituting back automatically.
 Indeed we can simply write:
 
@@ -820,7 +820,7 @@ variables appearing in the instance that should be generalized in the
 goal, so that they can vary in the induction hypotheses. By default, all
 variables appearing inside constructors (except in a parameter position)
 of the instantiated hypothesis will be generalized automatically but
-one can always give the list explicitely.
+one can always give the list explicitly.
 
 \begin{coq_example}
   Show.
@@ -829,7 +829,7 @@ one can always give the list explicitely.
 The {\tt simpl\_depind} tactic includes an automatic tactic that tries
 to simplify equalities appearing at the beginning of induction
 hypotheses, generally using trivial applications of
-reflexiviy. In cases where the equality is not between constructor
+reflexivity. In cases where the equality is not between constructor
 forms though, one must help the automation by giving
 some arguments, using the {\tt specialize} tactic.
 
@@ -949,7 +949,7 @@ Inductive formula : Type :=
   | f_or : formula -> formula -> formula
   | f_not : formula -> formula (* unary constructor *)
   | f_true : formula (* 0-ary constructor *)
-  | f_const : Prop -> formula (* contructor for constants *).
+  | f_const : Prop -> formula (* constructor for constants *).
 Fixpoint interp_f (f:
                    formula) : Prop :=
   match f with
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 126af9a5d..20c8c02b7 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -14,7 +14,7 @@ equivalences (e.g. rewriting systems).
 This documentation is adapted from the previous setoid documentation by
 Claudio Sacerdoti Coen (based on previous work by Cl\'ement Renard).
 The new implementation is a drop-in replacement for the old one \footnote{Nicolas
-Tabareau helped with the glueing}, hence most of the documentation still applies.
+Tabareau helped with the gluing}, hence most of the documentation still applies.
 
 The work is a complete rewrite of the previous implementation, based on
 the type class infrastructure. It also improves on and generalizes
@@ -203,7 +203,7 @@ have a type convertible to \texttt{reflexive (A $t_1$ \ldots $t_n$) (Aeq $t'_1$
   $t'_n$)}. Each proof may refer to the introduced variables as well. 
 
 \begin{cscexample}[Parametric relation]
-For leibniz equality, we may declare:
+For Leibniz equality, we may declare:
 \texttt{Add Parametric Relation (A : Type) :} \texttt{A (@eq A)}\\
 ~\zeroone{\texttt{reflexivity proved by} \texttt{@refl\_equal A}}\\
 \ldots
@@ -392,7 +392,7 @@ Contrary to the previous implementation, no specific error message will
 be raised when trying to replace a term that occurs in the wrong
 position. It will only fail because the rewriting constraints are not
 satisfiable. However it is possible to use the \texttt{at} modifier to
-specify which occurences should be rewritten.
+specify which occurrences should be rewritten.
 
 As expected, composing morphisms together propagates the variance annotations by
 switching the variance every time a contravariant position is traversed.
@@ -637,7 +637,7 @@ One then has to show that if two predicates are equivalent at every
 point, their universal quantifications are equivalent. Once we have
 declared such a morphism, it will be used by the setoid rewriting tactic
 each time we try to rewrite under an \texttt{all} application (products
-in \Prop{} are implicitely translated to such applications).
+in \Prop{} are implicitly translated to such applications).
 
 Indeed, when rewriting under a lambda, binding variable $x$, say from
 $P~x$ to $Q~x$ using the relation \texttt{iff}, the tactic will generate