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 /theories | |
| 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 'theories')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 2 | ||||
| -rw-r--r-- | theories/PArith/BinPosDef.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 9e8f44c0fb..fa33c1bf47 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -370,7 +370,7 @@ Fixpoint map_option (elt elt' : Type)(f : key -> elt -> option elt')(m : t elt) (** * Optimized map2 Suggestion by B. Gregoire: a [map2] function with specialized - arguments allowing to bypass some tree traversal. Instead of one + arguments that allows bypassing some tree traversal. Instead of one [f0] of type [key -> option elt -> option elt' -> option elt''], we ask here for: - [f] which is a specialisation of [f0] when first option isn't [None] diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 4f8d9ee27b..fcc12ab456 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -18,7 +18,7 @@ Require Export BinNums. -(** Postfix notation for positive numbers, allowing to mimic +(** Postfix notation for positive numbers, which allows mimicking the position of bits in a big-endian representation. For instance, we can write [1~1~0] instead of [(xO (xI xH))] for the number 6 (which is 110 in binary notation). @@ -557,4 +557,4 @@ Fixpoint of_succ_nat (n:nat) : positive := | S x => succ (of_succ_nat x) end. -End Pos.
\ No newline at end of file +End Pos. |