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 /doc | |
| 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 'doc')
| -rw-r--r-- | doc/faq/FAQ.tex | 2 | ||||
| -rw-r--r-- | doc/refman/Micromega.tex | 2 | ||||
| -rw-r--r-- | doc/refman/Setoid.tex | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 5806e9d72d..fba210c690 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -1644,7 +1644,7 @@ is a strong specification, using the \texttt{sumbool} type (look at the reference manual or chapter 9 of \cite{coqart}). Eliminations of the form ``~\texttt{case (le\_lt\_dec n p)}~'' provide proofs of -either $n \leq p$ or $p < n$, allowing to prove easily theorems as in +either $n \leq p$ or $p < n$, allowing easy proofs of some theorems as in question~\ref{minmax}. Unfortunately, this not the case of your \texttt{my\_le\_lt\_dec}, which returns a quite non-informative boolean value. diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 7bdbd6d84e..c9180b40c5 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -15,7 +15,7 @@ The {\tt Psatz} module ({\tt Require Psatz.}) gives access to several tactics fo \item {\tt psatz D n} where {\tt D} is {\tt Z}, {\tt Q} or {\tt R} and {\tt n} is an optional integer limiting the proof search depth is is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Sources and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} driver is generating - a \emph{proof cache} thus allowing to rerun scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). + a \emph{proof cache} which allows rerunning scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). \end{itemize} The tactics solve propositional formulas parameterised by atomic arithmetics expressions diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex index 55915189ce..ca416d7b1f 100644 --- a/doc/refman/Setoid.tex +++ b/doc/refman/Setoid.tex @@ -9,7 +9,7 @@ to work over user-defined structures (called setoids) that are equipped with ad-hoc equivalence relations meant to behave as equalities. Actually, the tactics have also been generalized to relations weaker then equivalences (e.g. rewriting systems). The toolbox also extends the -automatic rewriting capabilities of the system, allowing to specify +automatic rewriting capabilities of the system, allowing the specification of custom strategies for rewriting. This documentation is adapted from the previous setoid documentation by |