From bc6e87572b33eb5d98cbb23522a71fd7d23931b7 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 12 Aug 2014 08:51:59 -0400
Subject: 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.
---
 doc/faq/FAQ.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/faq/FAQ.tex')

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.
-- 
cgit v1.2.3

