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

4 files changed, 4 insertions, 4 deletions

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