Grammar: "allowing to" is not proper English

I'm not quite sure why, but I'm pretty sure it's not.  Rather, in
"allowing for foo" and "allowing to foo", "foo" modifies the sense in
which someting is allowed, rather than it being "foo" that's allowed.
"Allowing fooing" generally works, though it can sound a bit awkward.
"Allowing one to foo" (or "Allowing {him,her,it,Coq} to foo") is always
acceptable, in-as-much as it's ok to use "one".

I haven't touched the older instances of it in the CHANGES file.

1 files changed, 2 insertions, 2 deletions

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 7e4475d40..a1308e643 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -981,7 +981,7 @@ Inductive p_step : Set :=
   | P_NOP : p_step.
 
 (* List of normalizations to perform : with a constructor of type
-   [p_step] allowing to visit both left and right branches, we would be
+   [p_step] allowing the visiting of both left and right branches, we would be
    able to restrict to only one normalization by hypothesis.
    And since all hypothesis are useful (otherwise they wouldn't be included),
    we would be able to replace [h_step] by a simple list. *)
@@ -1014,7 +1014,7 @@ Inductive e_step : Set :=
 (* For each reified data-type, we define an efficient equality test.
    It is not the one produced by [Decide Equality].
 
-   Then we prove two theorem allowing to eliminate such equalities :
+   Then we prove two theorem allowing elimination of such equalities :
    \begin{verbatim}
    (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2.
    (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2.