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, 1 insertions, 1 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 5806e9d72d..fba210c690 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -1644,7 +1644,7 @@ is a strong specification, using the
 \texttt{sumbool} type (look at the reference manual or chapter 9 of
 \cite{coqart}). Eliminations of the form
 ``~\texttt{case (le\_lt\_dec n p)}~'' provide proofs of
-either $n \leq p$ or $p < n$, allowing to prove easily theorems as in
+either $n \leq p$ or $p < n$, allowing easy proofs of some theorems as in
 question~\ref{minmax}. Unfortunately, this not the case of your
 \texttt{my\_le\_lt\_dec}, which returns a quite non-informative boolean
 value.