diff options
| author | Jason Gross | 2014-08-12 08:51:59 -0400 |
|---|---|---|
| committer | Pierre Boutillier | 2014-08-25 15:22:40 +0200 |
| commit | bc6e87572b33eb5d98cbb23522a71fd7d23931b7 (patch) | |
| tree | 72ea727fcd6e704c88e92c52469fa293da0ecc39 /CHANGES | |
| parent | 33545ec3d624385d9e574988f53120cbd9fe5a9a (diff) | |
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.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 |