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. --- theories/PArith/BinPosDef.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/PArith') diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 4f8d9ee27..fcc12ab45 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. -- cgit v1.2.3