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. --- plugins/romega/ReflOmegaCore.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/romega') diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 7e4475d40..a1308e643 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -981,7 +981,7 @@ Inductive p_step : Set := | P_NOP : p_step. (* List of normalizations to perform : with a constructor of type - [p_step] allowing to visit both left and right branches, we would be + [p_step] allowing the visiting of both left and right branches, we would be able to restrict to only one normalization by hypothesis. And since all hypothesis are useful (otherwise they wouldn't be included), we would be able to replace [h_step] by a simple list. *) @@ -1014,7 +1014,7 @@ Inductive e_step : Set := (* For each reified data-type, we define an efficient equality test. It is not the one produced by [Decide Equality]. - Then we prove two theorem allowing to eliminate such equalities : + Then we prove two theorem allowing elimination of such equalities : \begin{verbatim} (t1,t2: typ) (eq_typ t1 t2) = true -> t1 = t2. (t1,t2: typ) (eq_typ t1 t2) = false -> ~ t1 = t2. -- cgit v1.2.3