aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/README
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2014-08-12 08:51:59 -0400
committerGravatar Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr>2014-08-25 15:22:40 +0200
commitbc6e87572b33eb5d98cbb23522a71fd7d23931b7 (patch)
tree72ea727fcd6e704c88e92c52469fa293da0ecc39 /plugins/extraction/README
parent33545ec3d624385d9e574988f53120cbd9fe5a9a (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 'plugins/extraction/README')
-rw-r--r--plugins/extraction/README2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/README b/plugins/extraction/README
index 64c871fd3..a9a7b04d5 100644
--- a/plugins/extraction/README
+++ b/plugins/extraction/README
@@ -6,7 +6,7 @@
What is it ?
------------
-The extraction is a mechanism allowing to produce functional code
+The extraction is a mechanism that produces functional code
(Ocaml/Haskell/Scheme) out of any Coq terms (either programs or
proofs).