diff options
| author |  Jason Gross <jgross@mit.edu> | 2014-08-12 08:51:59 -0400 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> | 2014-08-25 15:22:40 +0200 |
| commit | bc6e87572b33eb5d98cbb23522a71fd7d23931b7 (patch) | |
| tree | 72ea727fcd6e704c88e92c52469fa293da0ecc39 /doc/refman/Micromega.tex | |
| 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/refman/Micromega.tex')
| -rw-r--r-- | doc/refman/Micromega.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 7bdbd6d84..c9180b40c 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 |