"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).

54 files changed, 100 insertions, 100 deletions

diff --git a/.mailmap b/.mailmap
index a86b0c818..bb26f8517 100644
--- a/.mailmap
+++ b/.mailmap
@@ -1,6 +1,6 @@
 ## Coq contributors
 ##
-## This file allows to join the different accounts of a same person.
+## This file allows joining the different accounts of a same person.
 ## Cf for instance: git shortlog -nse. More details via: man git shortlog
 ##
 ## To avoid spam issues, we use by default a pseudo-email <login@gforge>
diff --git a/CHANGES b/CHANGES
index 25ae197b6..18c5a5350 100644
--- a/CHANGES
+++ b/CHANGES
@@ -37,7 +37,7 @@ Vernacular commands
 
 - The command "Record foo ..." does not generate induction principles
   (foo_rect, foo_rec, foo_ind) anymore by default (feature wish #2693).
-  A flag "Set/Unset Record Elimination Schemes" allows to change this.
+  A flag "Set/Unset Record Elimination Schemes" allows changing this.
   The tactic "induction" on a record is now actually doing "destruct".
 - The "Open Scope" command can now be given also a delimiter (e.g. Z).
 - The "Definition" command now allows the "Local" modifier, allowing
@@ -50,7 +50,7 @@ Vernacular commands
   recursively added to the load path, so files from installed libraries
   now need to be fully qualified for the "Require" command to find them.
   The tools/update-require script can be used to convert a development.
-- A new Print Strategies command allows to visualize the opacity status
+- A new Print Strategies command allows visualizing the opacity status
   of the whole engine.
 - The "Locate" command now searches through all sorts of qualified namespaces of
   Coq: terms, modules, tactics, etc. The old behaviour of the command can be
@@ -82,7 +82,7 @@ Tactics
     the need of the undocumented "contructor <tac>" syntax which is
     now equivalent to "once (constructor; tac)". (potential source of
     rare incompatibilities).
-  * New selector all: to qualify a tactic allows to apply a tactic to
+  * New selector all: to qualify a tactic allows applying a tactic to
     all the focused goal, instead of just the first one as is the
     default.
   * A corresponding new option Set Default Goal Selector "all" makes
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 49d78a7a6..c8373737c 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -211,7 +211,7 @@ let allowed_sorts issmall isunit s =
 
   (* Unitary/empty Prop: elimination to all sorts are realizable *)
   (* unless the type is large. If it is large, forbids large elimination *)
-  (* which otherwise allows to simulate the inconsistent system Type:Type *)
+  (* which otherwise allows simulating the inconsistent system Type:Type *)
   | InProp when isunit -> if issmall then all_sorts else small_sorts
 
   (* Other propositions: elimination only to Prop *)
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.
diff --git a/ide/coqide.ml b/ide/coqide.ml
index b0d90f2cb..ba20c771a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1377,7 +1377,7 @@ let check_for_geoproof_input () =
     full name, with the last occurrence of "coqide" replaced by "coqtop".
     This should correctly handle the ".opt", ".byte", ".exe" situations.
     If the replacement fails, we default to "coqtop", hoping it's somewhere
-    in the path. Note that the -coqtop option to coqide allows to override
+    in the path. Note that the -coqtop option to coqide overrides
     this default coqtop path *)
 
 let read_coqide_args argv =
diff --git a/ide/utils/config_file.mli b/ide/utils/config_file.mli
index b9c776828..22328e7f1 100644
--- a/ide/utils/config_file.mli
+++ b/ide/utils/config_file.mli
@@ -141,8 +141,8 @@ exception Missing_cp of groupable_cp
 or used to generate command line arguments.
 
 The basic usage is to have only one group and one configuration file,
-but this mechanism allows to have more,
-for instance to have another smaller group for the options to pass on the command line.
+but this mechanism allows having more,
+for instance having another smaller group for the options to pass on the command line.
 *)
 class group : object
   (** Adds a cp to the group.
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index ad12ad5fd..c1062a9db 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -67,7 +67,7 @@ let html_config_file_and_option () =
 let last_dir = ref "";;
 
 (** This function allows the user to select a file and returns the
-   selected file name. An optional function allows to change the
+   selected file name. An optional function allows changing the
    behaviour of the ok button.
    A VOIR : mutli-selection ? *)
 let select_files ?dir
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ee3a0dcf1..238eeb82e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -224,7 +224,7 @@ type section_subset_expr =
 
 type section_subset_descr = SsAll | SsType | SsExpr of section_subset_expr
 
-(* This type allows to register inline of constants in native compiler.
+(* This type allows registering the inlining of constants in native compiler.
    It will be extended with primitive inductive types and operators *)
 type register_kind = 
   | RegisterInline
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 894f88710..36a022fd9 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -50,7 +50,7 @@ open Pre_env
 (* Access to these variables is performed by the [Koffsetclosure n]       *)
 (* instruction that shifts the environment pointer of [n] fields.         *)
 
-(* This allows to represent mutual fixpoints in just one block.           *)
+(* This allows representing mutual fixpoints in just one block.           *)
 (* [Ct1 | ... | Ctn] is an array holding code pointers of the fixpoint    *)
 (* types. They are used in conversion tests (which requires that          *)
 (* fixpoint types must be convertible). Their environment is the one of   *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ff5ce284e..18ebc2aa0 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -220,7 +220,7 @@ let typecheck_inductive env ctx mie =
   let env' = push_context ctx env in
   let (env_params, params) = infer_local_decls env' mie.mind_entry_params in
   (* We first type arity of each inductive definition *)
-  (* This allows to build the environment of arities and to share *)
+  (* This allows building the environment of arities and to share *)
   (* the set of constraints *)
   let env_arities, rev_arity_list =
     List.fold_left
@@ -633,7 +633,7 @@ let allowed_sorts is_smashed s =
 (* Previous comment: *)
 (* Unitary/empty Prop: elimination to all sorts are realizable *)
 (* unless the type is large. If it is large, forbids large elimination *)
-(* which otherwise allows to simulate the inconsistent system Type:Type. *)
+(* which otherwise allows simulating the inconsistent system Type:Type. *)
 (* -> this is now handled by is_smashed: *)
 (* - all_sorts in case of small, unitary Prop (not smashed) *)
 (* - logical_sorts in case of large, unitary Prop (smashed) *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 9140d171d..bac242f82 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -99,7 +99,7 @@ val check_cofix : env -> cofixpoint -> unit
 
 (** {6 Support for sort-polymorphic inductive types } *)
 
-(** The "polyprop" optional argument below allows to control
+(** The "polyprop" optional argument below controls
     the "Prop-polymorphism". By default, it is allowed.
     But when "polyprop=false", the following exception is raised
     when a polymorphic singleton inductive type becomes Prop due to
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 466380f2d..5a2f5ced7 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -19,7 +19,7 @@ open Term
 (* Type declarations, these types shouldn't be exported they are accessed
    through specific functions. As being mutable and all it is wiser *)
 (* These types are put into two distinct categories: proactive and reactive.
-   Proactive information allows to find the name of a combinator, constructor
+   Proactive information allows finding the name of a combinator, constructor
    or inductive type handling a specific function.
    Reactive information is, on the other hand, everything you need to know
    about a specific name.*)
diff --git a/lib/cArray.mli b/lib/cArray.mli
index e3a3bd7f5..28f5110ee 100644
--- a/lib/cArray.mli
+++ b/lib/cArray.mli
@@ -126,5 +126,5 @@ sig
 end
 (** The functions defined in this module are the same as the main ones, except
     that they are all higher-order, and their function arguments have an
-    additional parameter. This allows to prevent closure creation in critical
+    additional parameter. This allows us to prevent closure creation in critical
     cases. *)
diff --git a/lib/cMap.mli b/lib/cMap.mli
index 4009ec99e..4a95c2346 100644
--- a/lib/cMap.mli
+++ b/lib/cMap.mli
@@ -54,7 +54,7 @@ sig
   module Unsafe :
   sig
     val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t
-    (** As the usual [map], but also allows to modify the key of a binding.
+    (** As the usual [map], but also allows modifying the key of a binding.
         It is required that the mapping function [f] preserves key equality,
         i.e.: for all (k : key) (x : 'a), compare (fst (f k x)) k = 0. *)
   end
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 9b72c3e9f..3f5443e03 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -796,7 +796,7 @@ let branch_as_cst (l,_,c) =
    When searching for the best factorisation below, we'll try both.
 *)
 
-(* The following structure allows to record which element occurred
+(* The following structure allows recording which element occurred
    at what position, and then finally return the most frequent
    element and its positions. *)
 
diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 41b5ec545..b84cf2540 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -990,7 +990,7 @@ Inductive h_step : Set :=
     pair_step : nat -> p_step -> h_step.
 
 (* \subsubsection{Rules for decomposing the hypothesis} *)
-(* This type allows to navigate in the logical constructors that
+(* This type allows navigation in the logical constructors that
    form the predicats of the hypothesis in order to decompose them.
    This allows in particular to extract one hypothesis from a
    conjunction with possibly the right level of negations. *)
@@ -1000,7 +1000,7 @@ Inductive direction : Set :=
   | D_right : direction
   | D_mono : direction.
 
-(* This type allows to extract useful components from hypothesis, either
+(* This type allows extracting useful components from hypothesis, either
    hypothesis generated by splitting a disjonction, or equations.
    The last constructor indicates how to solve the obtained system
    via the use of the trace type of Omega [t_omega] *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index b7be2c0f5..7dd59cf05 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -18,7 +18,7 @@ open Goptions
     - The "short" one, that just prints the names of the fields.
     - The "rich" one, that also tries to print the types of the fields.
     The short version used to be the default behavior, but now we print
-    types by default. The following option allows to change this.
+    types by default. The following option allows changing this.
     Technically, the environments in this file are either None in
     the "short" mode or (Some env) in the "rich" one.
 *)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 4472bbcb7..234c3fff9 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -451,7 +451,7 @@ module Refine : sig
 
 end
 
-(* The [NonLogical] module allows to execute side effects in tactics
+(* The [NonLogical] module allows the execution of side effects in tactics
    (non-logical side-effects are not discarded at failures). *)
 module NonLogical : sig
 
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index 21a9722d2..631667282 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* Compiling the theories allows to test parsing and typing but not printing *)
+(* Compiling the theories allows testing parsing and typing but not printing *)
 (* This file tests that pretty-printing does not fail                        *)
 (* Test of exact output is not specified                                     *)
 
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 1393843ec..25367a10f 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -164,8 +164,8 @@ intros.
 apply H with (y:=y).
 (* [x] had two possible instances: [S 0], coming from unifying the
    type of [y] with [I ?n] and [succ 0] coming from the unification with
-   the goal; only the first one allows to make the next apply (which
-   does not work modulo delta) working *)
+   the goal; only the first one allows the next apply (which
+   does not work modulo delta) work *)
 apply H0.
 Qed.
 
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 44e4808b8..04edcd7ec 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -38,7 +38,7 @@ Lemma predicate_implication_pointwise (l : Tlist) :
   Proper (@predicate_implication l ==> pointwise_lifting impl l) id.
 Proof. do 2 red. unfold predicate_implication. auto. Qed.
 
-(** The instantiation at relation allows to rewrite applications of relations
+(** The instantiation at relation allows rewriting applications of relations
     [R x y] to [R' x y]  when [R] and [R'] are in [relation_equivalence]. *)
 
 Instance relation_equivalence_pointwise :
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 23d9d10eb..56a0661ed 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -68,7 +68,7 @@ Ltac absurd_hyp H :=
   let T := type of H in
   absurd T.
 
-(* A useful complement to contradict. Here H:A while G allows to conclude ~A *)
+(* A useful complement to contradict. Here H:A while G allows concluding ~A *)
 
 Ltac false_hyp H G :=
   let T := type of H in absurd T; [ apply G | assumption ].
diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v
index 3e5d4ef0c..0fcbae42c 100644
--- a/theories/Logic/Description.v
+++ b/theories/Logic/Description.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (** This file provides a constructive form of definite description; it
-    allows to build functions from the proof of their existence in any
+    allows building functions from the proof of their existence in any
     context; this is weaker than Church's iota operator *)
 
 Require Import ChoiceFacts.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 4dfe99504..0d202eab5 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -320,7 +320,7 @@ Section Equivalences.
    [Definition Eq_rec_eq :=
       forall (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h.]
 
-    Typically, [eq_rect_eq] allows to prove UIP and Streicher's K what
+    Typically, [eq_rect_eq] allows proving UIP and Streicher's K what
     does not seem possible with [eq_rec_eq]. In particular, the proof of [UIP]
     requires to use [eq_rect_eq] on [fun y -> x=y] which is in [Type] but not
     in [Set].
diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v
index 5424eea82..c1a1a31d7 100644
--- a/theories/Logic/IndefiniteDescription.v
+++ b/theories/Logic/IndefiniteDescription.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 (** This file provides a constructive form of indefinite description that
-    allows to build choice functions; this is weaker than Hilbert's
+    allows building choice functions; this is weaker than Hilbert's
     epsilon operator (which implies weakly classical properties) but
     stronger than the axiom of choice (which cannot be used outside
     the context of a theorem proof). *)
diff --git a/theories/Logic/SetIsType.v b/theories/Logic/SetIsType.v
index c0a6f9edc..4e36f8cb0 100644
--- a/theories/Logic/SetIsType.v
+++ b/theories/Logic/SetIsType.v
@@ -9,7 +9,7 @@
 (** * The Set universe seen as a synonym for Type *)
 
 (** After loading this file, Set becomes just another name for Type.
-    This allows to easily perform a Set-to-Type migration, or at least
+    This allows easily performing a Set-to-Type migration, or at least
     test whether a development relies or not on specific features of
     Set: simply insert some Require Export of this file at starting
     points of the development and try to recompile...  *)
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 25d899029..e1fc454ae 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -312,7 +312,7 @@ Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
 Local Hint Resolve elements_spec2.
 
 (* Sometimes functional induction will expose too much of
-   a tree structure. The following tactic allows to factor back
+   a tree structure. The following tactic allows factoring back
    a Node whose internal parts occurs nowhere else. *)
 
 (* TODO: why Ltac instead of Tactic Notation don't work ? why clear ? *)
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 1be361b66..98f84a60c 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -654,7 +654,7 @@ Section Basics.
  f_equal; auto.
  Qed.
 
- (** This equivalence allows to prove easily the following delicate
+ (** This equivalence allows proving easily the following delicate
      result *)
 
  Lemma EqShiftL_twice_plus_one : forall k x y,
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index 26d5ffef0..e8fd2c6b3 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -30,7 +30,7 @@ Module Type NZPowSpec (Import A : NZOrdAxiomsSig')(Import B : Pow' A).
 End NZPowSpec.
 
 (** The above [pow_neg_r] specification is useless (and trivially
-   provable) for N. Having it here allows to already derive
+   provable) for N. Having it here already allows deriving
    some slightly more general statements. *)
 
 Module Type NZPow (A : NZOrdAxiomsSig) := Pow A <+ NZPowSpec A.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index f98e8da9a..afd685ba9 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -24,7 +24,7 @@ Variable A : Type.
 Variable Aeq : relation A.
 Variable Aeq_equiv : Equivalence Aeq.
 
-(** [strong_rec] allows to define a recursive function [phi] given by
+(** [strong_rec] allows defining a recursive function [phi] given by
     an equation [phi(n) = F(phi)(n)] where recursive calls to [phi]
     in [F] are made on strictly lower numbers than [n].
 
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index 50c90757a..e866a52d6 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -33,7 +33,7 @@ Module BigN_BigZ <: NType_ZType BigN.BigN BigZ.
  Qed.
 End BigN_BigZ.
 
-(** This allows to build [BigQ] out of [BigN] and [BigQ] via [QMake] *)
+(** This allows building [BigQ] out of [BigN] and [BigQ] via [QMake] *)
 
 Delimit Scope bigQ_scope with bigQ.
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index b9510342c..cc8c2261b 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -49,7 +49,7 @@ Module Type OrderedType.
   Include MiniOrderedType.
 
   (** A [eq_dec] can be deduced from [compare] below. But adding this
-     redundant field allows to see an OrderedType as a DecidableType. *)
+     redundant field allows seeing an OrderedType as a DecidableType. *)
   Parameter eq_dec : forall x y, { eq x y } + { ~ eq x y }.
 
 End OrderedType.
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index e179bd8b4..724690b42 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -95,7 +95,7 @@ Module Type OrderedTypeFull' :=
  OrderedTypeFull <+ EqLtLeNotation <+ CmpNotation.
 
 (** NB: in [OrderedType], an [eq_dec] could be deduced from [compare].
-  But adding this redundant field allows to see an [OrderedType] as a
+  But adding this redundant field allows seeing an [OrderedType] as a
   [DecidableType]. *)
 
 (** * Versions with [eq] being the usual Leibniz equality of Coq *)
diff --git a/tools/gallina-db.el b/tools/gallina-db.el
index dd2bdf3ff..baabebb13 100644
--- a/tools/gallina-db.el
+++ b/tools/gallina-db.el
@@ -48,7 +48,7 @@ Is ok because the longer regexp is recognized first.
 
 If non-nil the optional INSERT-FUN is the function to be called when inserting
 the form (instead of inserting INSERT, except when using \\[expand-abbrev]). This
-allows to write functions asking for more information to assist the user.
+allows writing functions asking for more information to assist the user.
 
 If non-nil the optional HIDE specifies that this form should not appear in the
 menu but only in interactive completions.