"allows to", like "allowing to", is improper

It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).

21 files changed, 61 insertions, 61 deletions

diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index 857ba84d7..0d727e170 100644
--- a/doc/RecTutorial/RecTutorial.tex
+++ b/doc/RecTutorial/RecTutorial.tex
@@ -2689,7 +2689,7 @@ then appear as subgoals that remain to be solved.
 In the previous proof, the tactic call ``~\citecoq{apply nat\_ind with (P:= fun n {\funarrow} n {\coqdiff} S n)}~'' can simply be replaced with ``~\citecoq{elim n}~''.
 
 The option ``~\citecoq{\texttt{elim} $t$ \texttt{using} $C$}~''
- allows to use a
+ allows the use of a
 derived combinator $C$ instead of the default one. Consider the
 following theorem, stating that equality is decidable on natural
 numbers:
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex
index fab660711..28a6f6903 100644
--- a/doc/refman/CanonicalStructures.tex
+++ b/doc/refman/CanonicalStructures.tex
@@ -38,7 +38,7 @@ Module EQ.
 End EQ.
 \end{coq_example}
 
-We use Coq modules as name spaces.  This allows to follow the same pattern
+We use Coq modules as name spaces.  This allows us to follow the same pattern
 and naming convention for the rest of the chapter.  The base name space
 contains the definitions of the algebraic structure.  To keep the example
 small, the algebraic structure $EQ.type$ we are defining is very simplistic,
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 888aba175..2552feef9 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -75,7 +75,7 @@ Fixpoint max (n m:nat) {struct m} : nat :=
 
 \paragraph{Multiple patterns}
 
-Using multiple patterns in the definition of {\tt max} allows to write:
+Using multiple patterns in the definition of {\tt max} lets us write:
 
 \begin{coq_example}
 Reset max.
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index ea1ae02bc..869ba971c 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -403,7 +403,7 @@ This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_in
 \comindex{Typeclasses eauto}
 \label{TypeclassesEauto}
 
-This commands allows to customize the type class resolution tactic,
+This command allows customization of the type class resolution tactic,
 based on a variant of eauto. The flags semantics are:
 \begin{itemize}
 \item {\tt debug} In debug mode, the trace of successfully applied
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 53ef490ff..37326c10f 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -150,7 +150,7 @@ Default is Unset. Normaly, when the extraction of an inductive type
 produces a singleton type (i.e. a type with only one constructor, and
 only one argument to this constructor), the inductive structure is
 removed and this type is seen as an alias to the inner type.
-The typical example is {\tt sig}. This option allows to disable this
+The typical example is {\tt sig}. This option allows disabling this
 optimization when one wishes to preserve the inductive structure of types.
 
 \item \comindex{Set Extraction AutoInline}
@@ -219,7 +219,7 @@ this constant is not declared in the generated file.
 \item \comindex{Extraction Implicit}
  {\tt Extraction Implicit} \qualid\ [ \ident$_1$ \dots\ \ident$_n$ ].
 
-This experimental command allows to declare some arguments of
+This experimental command allows declaring some arguments of
 \qualid\ as implicit, i.e. useless in extracted code and hence to
 be removed by extraction. Here \qualid\ can be any function or
 inductive constructor, and \ident$_i$ are the names of the concerned
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index f8f456fa8..b0c328a54 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -17,7 +17,7 @@ We call this calculus the
   Constructions}\index{Predicative Calculus of
   (Co)Inductive Constructions} (\pCIC\ in short).
 In Section~\ref{impredicativity} we give the extra-rules for \iCIC. A
-  compiling option of \Coq{} allows to type-check theories in this
+  compiling option of \Coq{} allows type-checking theories in this
   extended system.
 
 In \CIC\, all objects have a {\em type}. There are types for functions (or
@@ -31,7 +31,7 @@ written {\it ``x:T''}. One also says: {\it ``x has type T''}.
 The terms of {\CIC} are detailed in Section~\ref{Terms}.
 
 In \CIC\, there is an internal reduction mechanism. In particular, it
-allows to decide if two programs are {\em intentionally} equal (one
+can decide if two programs are {\em intentionally} equal (one
 says {\em convertible}). Convertibility is presented in section 
 \ref{convertibility}.
 
@@ -447,7 +447,7 @@ recursively convertible to $u'_1$, or, symmetrically, $u_2$ is $\lb
 x:T\mto u'_2$ and $u_1\,x$ is recursively convertible to $u'_2$.  We
 then write $\WTEGCONV{t_1}{t_2}$.
 
-The convertibility relation allows to introduce a new typing rule
+The convertibility relation allows introducing a new typing rule
 which says that two convertible well-formed types have the same
 inhabitants.
 
diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex
index d75b9eb93..4ef5818aa 100644
--- a/doc/refman/RefMan-coi.tex
+++ b/doc/refman/RefMan-coi.tex
@@ -286,7 +286,7 @@ Reset eqproof.
 \noindent Instead of giving an explicit definition, 
 we can use the proof editor of Coq to help us in 
 the construction of the proof.
-A tactic \verb!Cofix! allows to place a \verb!CoFixpoint! definition
+A tactic \verb!Cofix! allows placing a \verb!CoFixpoint! definition
 inside a proof. 
 This tactic introduces a variable in the context which has
 the same type as the current goal, and its application stands
@@ -331,8 +331,8 @@ with the tactic \verb!Cofix!. Remark that once it has been used
 the application of tactics performing automatic proof search in 
 the environment (like for example \verb!Auto!)
 could introduce unguarded recursive calls in the proof.
-The command \verb!Guarded! allows to verify 
-if the guarded condition has been violated 
+The command \verb!Guarded! verifies
+that the guarded condition has been not violated 
 during the construction of the proof. This command can be
 applied even if the proof term is not complete.
 
diff --git a/doc/refman/RefMan-decl.tex b/doc/refman/RefMan-decl.tex
index 9015b8ec3..292b8bbed 100644
--- a/doc/refman/RefMan-decl.tex
+++ b/doc/refman/RefMan-decl.tex
@@ -53,7 +53,7 @@ experience using the \DPL .
 \item The focusing mechanism is constrained so that only one goal at
   a time is visible.
 \item Giving a statement that Coq cannot prove does not produce an
-  error, only a warning: this allows to go on with the proof and fill
+  error, only a warning: this allows going on with the proof and fill
   the gap later.
 \item Tactics can still be used for justifications and after
 {\texttt{escape}}.
@@ -224,7 +224,7 @@ inside a procedural proof inside a mathematical proof ...
 
 \subsection{Computation steps}
 
-The {\tt reconsider ... as} command allows to change the type of a hypothesis or of {\tt thesis} to a convertible one.
+The {\tt reconsider ... as} command allows changing the type of a hypothesis or of {\tt thesis} to a convertible one.
 
 \begin{coq_eval}
 Theorem T: let a:=false in let b:= true in ( if a then True else False -> if b then True else False).
@@ -478,7 +478,7 @@ Abort.
 \end{coq_eval}
 
 Now, an example with the {\tt suffices} command. {\tt suffices}
-is a sort of dual for {\tt have}: it allows to replace the conclusion
+is a sort of dual for {\tt have}: it allows replacing the conclusion
 (or part of it) by a sufficient condition. 
 
 \begin{coq_eval}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 8a5e8bb07..c4163b3b0 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -14,7 +14,7 @@ records as is done in many programming languages.  Its syntax is
 described on Figure~\ref{record-syntax}.  In fact, the \verb+Record+
 macro is more general than the usual record types, since it allows
 also for ``manifest'' expressions. In this sense, the \verb+Record+
-construction allows to define ``signatures''.
+construction allows defining ``signatures''.
 
 \begin{figure}[h]
 \begin{centerframe}
@@ -208,7 +208,7 @@ Record point := { x : nat; y : nat }.
 Definition a := Build_point 5 3.
 \end{coq_example}
 
-The following syntax allows to create objects by using named fields. The
+The following syntax allows creating objects by using named fields. The
 fields do not have to be in any particular order, nor do they have to be all
 present if the missing ones can be inferred or prompted for (see
 Section~\ref{Program}).
@@ -859,8 +859,8 @@ subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independe
 \index{Sections}
 \label{Section}}
 
-The sectioning mechanism allows to organize a proof in structured
-sections. Then local declarations become available (see
+The sectioning mechanism can be used to to organize a proof in
+structured sections. Then local declarations become available (see
 Section~\ref{Basic-definitions}).
 
 \subsection{\tt Section {\ident}\comindex{Section}}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 2f128abaa..b8e715c76 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -3,7 +3,7 @@
 \label{BNF-syntax} % Used referred to as a chapter label
 
 This chapter describes \gallina, the specification language of {\Coq}.
-It allows to develop mathematical theories and to prove specifications
+It allows developing mathematical theories and to prove specifications
 of programs.  The theories are built from axioms, hypotheses,
 parameters, lemmas, theorems and definitions of constants, functions,
 predicates and sets. The syntax of logical objects involved in
@@ -989,7 +989,7 @@ Check nat_ind.
 
 This is the well known structural induction principle over natural
 numbers, i.e. the second-order form of Peano's induction principle.
-It allows to prove some universal property of natural numbers ({\tt
+It allows proving some universal property of natural numbers ({\tt
 forall n:nat, P n}) by induction on {\tt n}.
 
 The types of {\tt nat\_rec} and {\tt nat\_rect} are similar, except
@@ -1327,7 +1327,7 @@ constructions. The command:
   \ident$_0$ {\tt \}} : type$_0$ := \term$_0$ 
   \comindex{Fixpoint}\label{Fixpoint}}
 \end{center}
-allows to define functions by pattern-matching over inductive objects 
+allows defining functions by pattern-matching over inductive objects 
 using a fixed point construction.
 The meaning of this declaration is to define {\it ident} a recursive
 function with arguments specified by the binders in {\params} such
@@ -1610,7 +1610,7 @@ The command can be used also with {\tt Lemma},
 
 \item {\tt Definition {\ident} \zeroone{\binders} : {\type}.}
 
-This allows to define a term of type {\type} using the proof editing mode. It
+This allows defining a term of type {\type} using the proof editing mode. It
 behaves as {\tt Theorem} but is intended to be used in conjunction with
   {\tt Defined} (see \ref{Defined}) in order to define a
  constant of which the computational behavior is relevant.
diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index ec640f4ef..c036f031f 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -120,7 +120,7 @@ insertion cursor.
  
 \section{Vernacular commands, templates}
 
-The \texttt{Templates} menu allows to use shortcuts to insert
+The \texttt{Templates} menu allows using shortcuts to insert
 vernacular commands. This is a nice way to proceed if you are not sure
 of the spelling of the command you want.
 
@@ -193,12 +193,12 @@ will be prompt to choose to either discard your changes or not. The
 Section~\ref{sec:coqidecharencoding}
  
 
-The \verb|Externals| section allows to customize the external commands
+The \verb|Externals| section allows customizing the external commands
 for compilation, printing, web browsing. In the browser command, you
 may use \verb|%s| to denote the URL to open, for example: %
 \verb|mozilla -remote "OpenURL(%s)"|. 
 
-The \verb|Tactics Wizard| section allows to defined the set of tactics
+The \verb|Tactics Wizard| section allows defining the set of tactics
 that should be tried, in sequence, to solve the current goal.
 
 The last section is for miscellaneous boolean settings, such as the
diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex
index 959442402..43bd2419f 100644
--- a/doc/refman/RefMan-ind.tex
+++ b/doc/refman/RefMan-ind.tex
@@ -229,7 +229,7 @@ Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and
 
 \item \texttt{Dependent Inversion\_clear } \ident~ \texttt{ with } \term\\
 \index{Dependent Inversion_clear...with@{\tt Dependent Inversion\_clear...with}}
- \noindent Behaves as \texttt{Dependent Inversion\_clear} but allows to give
+ \noindent Behaves as \texttt{Dependent Inversion\_clear} but allows giving
   explicitly the good 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
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index da2e099f9..5f1e11c47 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -998,7 +998,7 @@ discrR.
 Abort.
 \end{coq_eval}
 
-\item {\tt split\_Rabs} allows to unfold {\tt Rabs} constant and splits 
+\item {\tt split\_Rabs} allows unfolding the {\tt Rabs} constant and splits 
 corresponding conjunctions.
 \tacindex{split\_Rabs}
 
@@ -1015,7 +1015,7 @@ intro; split_Rabs.
 Abort.
 \end{coq_eval}
 
-\item {\tt split\_Rmult} allows to split a condition that a product is
+\item {\tt split\_Rmult} splits a condition that a product is
   non null into subgoals corresponding to the condition on each
   operand of the product. 
 \tacindex{split\_Rmult}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 13ff9afb1..cba664f4c 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -975,7 +975,7 @@ without having to cut manually the proof in smaller lemmas.
 \subsubsection[Calling an external tactic]{Calling an external tactic\tacindex{external}
 \index{Ltac!external}}
 
-The tactic {\tt external} allows to run an executable outside the
+The tactic {\tt external} runs an executable outside the
 {\Coq} executable. The communication is done via an XML encoding of
 constructions. The syntax of the command is
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 0a283776f..ac0193b2f 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -399,7 +399,7 @@ A lemma whose fully-qualified name contains any of the declared substrings
 will be removed from the search results.
 The default blacklisted substrings are {\tt "\_admitted"
   "\_subproof" "Private\_"}. The command {\tt Remove Search Blacklist
-  ...} allows to expunge this blacklist.
+  ...} allows expunging this blacklist.
 
 % \begin{tabbing}
 % \ \ \ \ \=11.\ \=\kill
@@ -877,7 +877,7 @@ extra commands and end on a state $\num' \leq \num$ if necessary.
 \begin{Variants}
 \item {\tt Backtrack $\num_1$ $\num_2$ $\num_3$}.\comindex{Backtrack}\\
   {\tt Backtrack} is a \emph{deprecated} form of {\tt BackTo} which
-  allows to explicitely manipulate the proof environment. The three
+  allows explicitely manipulating the proof environment. The three
   numbers $\num_1$, $\num_2$ and $\num_3$ represent the following:
 \begin{itemize}
 \item $\num_3$: Number of \texttt{Abort} to perform, i.e. the number
@@ -1121,7 +1121,7 @@ constant.
 
 \subsection{\tt Declare Reduction \ident\ := {\rm\sl convtactic}.}
 
-This command allows to give a short name to a reduction expression,
+This command allows giving a short name to a reduction expression,
 for instance {\tt lazy beta delta [foo bar]}. This short name can
 then be used in {\tt Eval \ident\ in ...} or {\tt eval} directives.
 This command accepts the {\tt Local} modifier, for discarding
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 52d8c09c1..c05fc829e 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -174,7 +174,7 @@ proof was edited.
 \subsection[\tt Existential {\num} := {\term}.]{\tt Existential  {\num} := {\term}.\comindex{Existential}
 \label{Existential}}
 
-This command allows to instantiate an existential variable. {\tt \num}
+This command instantiates an existential variable. {\tt \num}
 is an index in the list of uninstantiated existential variables
 displayed by {\tt Show Existentials.} (described in Section~\ref{Show})
 
@@ -395,7 +395,7 @@ of interactive proof construction, the check of the termination (or
 guardedness) of the recursive calls in the fixpoint or cofixpoint
 constructions is postponed to the time of the completion of the proof.
 
-The command \verb!Guarded! allows to verify if the guard condition for
+The command \verb!Guarded! allows checking if the guard condition for
 fixpoint and cofixpoint is violated at some time of the construction
 of the proof without having to wait the completion of the proof."
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 27f8e3024..aaca07321 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -443,7 +443,7 @@ apply (Rtrans _ m).
 Undo.
 \end{coq_eval}
 
-More elegantly, {\tt apply Rtrans with (y:=m)} allows to only mention
+More elegantly, {\tt apply Rtrans with (y:=m)} allows only mentioning
 the unknown {\tt m}:
 
 \begin{coq_example*}
@@ -1093,7 +1093,7 @@ matching the pattern.
 
 \item {\tt set ( {\ident} := {\term} ) in {\occgoalset}}
 
-This notation allows to specify which occurrences of {\term} have to
+This notation allows specifying which occurrences of {\term} have to
 be substituted in the context. The {\tt in {\occgoalset}} clause is an
 occurrence clause whose syntax and behavior are described in
 Section~\ref{Occurrences clauses}.
@@ -1151,7 +1151,7 @@ Section~\ref{Occurrences clauses}.
 \label{decompose}
 \tacindex{decompose}
 
-This tactic allows to recursively decompose a
+This tactic recursively decomposes a
 complex proposition in order to obtain atomic ones.
 
 \Example
@@ -1392,7 +1392,7 @@ existential variable.
 \tacindex{instantiate}
 \label{instantiate}
 
-The {\tt instantiate} tactic allows to refine (see Section~\ref{refine})
+The {\tt instantiate} tactic refines (see Section~\ref{refine})
 an existential variable
 with the term \term. The \num\  argument is the position of the
 existential variable from right to left in the conclusion. This cannot be
@@ -1430,7 +1430,7 @@ a hypothesis or in the body or the type of a local definition.
 \label{admit}
 
 The {\tt admit} tactic ``solves'' the current subgoal by an
-axiom. This typically allows to temporarily skip a subgoal so as to
+axiom. This typically allows temporarily skiping a subgoal so as to
 progress further in the rest of the proof. To know if some proof still
 relies on unproved subgoals, one can use the command {\tt Print
 Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals
@@ -1473,7 +1473,7 @@ The proof of {\tt False} is searched in the hypothesis named \ident.
 \label{contradict}
 \tacindex{contradict}
 
-This tactic allows to manipulate negated hypothesis and goals. The
+This tactic allows manipulating negated hypothesis and goals. The
 name \ident\ should correspond to a hypothesis. With
 {\tt contradict H}, the current goal and context is transformed in
 the following way:
@@ -1834,8 +1834,8 @@ induction n.
 
 Allows the user to give explicitly an elimination predicate
 {\term$_2$} that is not the standard one for the underlying inductive
-type of {\term$_1$}. The {\bindinglist} clause allows to
-instantiate premises of the type of {\term$_2$}.
+type of {\term$_1$}. The {\bindinglist} clause allows
+instantiating premises of the type of {\term$_2$}.
 
 \item{\tt elim {\term$_1$} with {\bindinglist$_1$} using {\term$_2$} with {\bindinglist$_2$}}\\
      {\tt eelim {\term$_1$} with {\bindinglist$_1$} using {\term$_2$} with {\bindinglist$_2$}}
@@ -2055,7 +2055,7 @@ details.
   as {\disjconjintropattern} using \term$_{m+1}$ with \bindinglist}
 
  Similarly to \texttt{Induction} and \texttt{elim}
- (see Section~\ref{Tac-induction}), this allows to give explicitly the
+ (see Section~\ref{Tac-induction}), this allows giving explicitly the
  name of the introduced variables, the
  induction principle, and the values of dependent premises of the
  elimination scheme, including \emph{predicates} for mutual induction
@@ -2312,13 +2312,13 @@ Abort.
 
 \item \texttt{inversion {\num} as \intropattern}
 
-  This allows to name the hypotheses introduced by
+  This allows naming the hypotheses introduced by
   \texttt{inversion \num} in the context.
 
 \item \tacindex{inversion\_clear \dots\ as} \texttt{inversion\_clear
   {\ident} as \intropattern}
 
-  This allows to name the hypotheses introduced by
+  This allows naming the hypotheses introduced by
   \texttt{inversion\_clear} in the context.
 
 \item \tacindex{inversion \dots\ in} \texttt{inversion {\ident}
@@ -2332,7 +2332,7 @@ Abort.
   {\ident} as {\intropattern} in \ident$_1$ \dots\
   \ident$_n$}
 
-  This allows to name the hypotheses introduced in the context by
+  This allows naming the hypotheses introduced in the context by
   \texttt{inversion {\ident} in \ident$_1$ \dots\ \ident$_n$}.
 
 \item \tacindex{inversion\_clear \dots\ in} \texttt{inversion\_clear
@@ -2346,7 +2346,7 @@ Abort.
   \texttt{inversion\_clear {\ident} as {\intropattern}
   in \ident$_1$ \dots\ \ident$_n$}
 
-  This allows to name the hypotheses introduced in the context by
+  This allows naming the hypotheses introduced in the context by
   \texttt{inversion\_clear {\ident} in \ident$_1$ \dots\ \ident$_n$}.
 
 \item \tacindex{dependent inversion} \texttt{dependent inversion \ident}
@@ -2358,7 +2358,7 @@ Abort.
 \item \tacindex{dependent inversion \dots\ as } \texttt{dependent
     inversion {\ident} as \intropattern}
 
-  This allows to name the hypotheses introduced in the context by
+  This allows naming the hypotheses introduced in the context by
   \texttt{dependent inversion} {\ident}.
 
 \item \tacindex{dependent inversion\_clear} \texttt{dependent
@@ -2370,7 +2370,7 @@ Abort.
 \item \tacindex{dependent inversion\_clear \dots\ as}
   \texttt{dependent inversion\_clear {\ident} as \intropattern}
 
-  This allows to name the hypotheses introduced in the context by
+  This allows naming the hypotheses introduced in the context by
   \texttt{dependent inversion\_clear} {\ident}.
 
 \item \tacindex{dependent inversion \dots\ with} \texttt{dependent
@@ -2387,7 +2387,7 @@ Abort.
   \texttt{dependent inversion {\ident} as {\intropattern}
   with \term}
 
-  This allows to name the hypotheses introduced in the context by
+  This allows naming the hypotheses introduced in the context by
   \texttt{dependent inversion {\ident} with \term}.
 
 \item \tacindex{dependent inversion\_clear \dots\ with}
@@ -2400,7 +2400,7 @@ Abort.
   \texttt{dependent inversion\_clear {\ident} as
   {\intropattern} with \term}
 
-  This allows to name the hypotheses introduced in the context by
+  This allows naming the hypotheses introduced in the context by
   \texttt{dependent inversion\_clear {\ident} with \term}.
 
 \item \tacindex{simple inversion} \texttt{simple inversion \ident}
@@ -2412,7 +2412,7 @@ Abort.
 \item \tacindex{simple inversion \dots\ as} \texttt{simple inversion
   {\ident} as \intropattern}
 
-  This allows to name the hypotheses introduced in the context by
+  This allows naming the hypotheses introduced in the context by
   \texttt{simple inversion}.
 
 \item \tacindex{inversion \dots\ using} \texttt{inversion {\ident}
@@ -4400,11 +4400,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
+  If 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
-  choose which must be inverted.
+  are valid candidates to functional inversion, this variant allows
+  choosing which {\qualid} is inverted.
 \end{Variants}
 
 
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 6667fd5a4..5703c73f0 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -345,7 +345,7 @@ Reset Initial.
 \section[\tt quote]{\tt quote\tacindex{quote}
 \label{quote-examples}}
 
-The tactic \texttt{quote} allows to use Barendregt's so-called
+The tactic \texttt{quote} allows using 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' 
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex
index 7de74ef95..ccd180db6 100644
--- a/doc/refman/Universes.tex
+++ b/doc/refman/Universes.tex
@@ -7,7 +7,7 @@
 \asection{General Presentation}
 
 This section describes the universe polymorphic extension of Coq.
-Universe polymorphism allows to write generic definitions making use of
+Universe polymorphism allows writing generic definitions making use of
 universes and reuse them at different and sometimes incompatible levels.
 
 A standard example of the difference between universe \emph{polymorphic} and 
diff --git a/doc/tools/Translator.tex b/doc/tools/Translator.tex
index 005ca9c0c..5f7b6dc95 100644
--- a/doc/tools/Translator.tex
+++ b/doc/tools/Translator.tex
@@ -78,8 +78,8 @@ strongly recommended to read first the definition of the new syntax
 (in the reference manual), but this document should also be useful for
 the eager user who wants to start with the new syntax quickly.
 
-The toplevel has an option {\tt -translate} which allows to
-interactively translate commands. This toplevel translator accepts a
+The toplevel has an option {\tt -translate} which allows
+interactively translating commands. This toplevel translator accepts a
 command, prints the translation on standard output (after a %
 \verb+New syntax:+ balise), executes the command, and waits for another
 command. The only requirements is that they should be syntactically
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 55ef730a5..de3d9c3f2 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -1554,7 +1554,7 @@ SearchHead le.
 \end{coq_example}
 
 A new and more convenient search tool is \textsf{SearchPattern}
-developed by Yves Bertot. It allows to find the theorems with a
+developed by Yves Bertot. It allows finding the theorems with a
 conclusion matching a given pattern, where \verb:\_: can be used in
 place of an arbitrary term. We remark in this example, that \Coq{}
 provides usual infix notations for arithmetic operators.