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

13 files changed, 13 insertions, 13 deletions

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 *)