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.
---
 CHANGES | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index bef29d3d16..25ae197b68 100644
--- a/CHANGES
+++ b/CHANGES
@@ -60,7 +60,7 @@ Vernacular commands
 Specification Language
 
 - Slight changes in unification error messages.
-- Added a syntax $(...)$ allowing to put tactics in terms.
+- Added a syntax $(...)$ that allows putting tactics in terms.
 - Constants in pattern-matching branches now respect the same rules regarding
   implicit arguments than in applicative position. The old behaviour can be
   recovered by the command "Set Asymmetric Patterns". (possible source of
-- 
cgit v1.2.3