"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, 5 insertions, 5 deletions

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