diff options
| author |  Jason Gross <jgross@mit.edu> | 2014-08-12 11:14:04 -0400 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> | 2014-08-25 15:22:40 +0200 |
| commit | 4fef230a1ee1964712e3ac7f325ce00968ac4769 (patch) | |
| tree | 7be49300bc9c989a4ec716685356cb8f5aab752e /doc/refman/RefMan-ext.tex | |
| parent | 876b1b39a0304c93c2511ca8dd34353413e91c9d (diff) | |
"allows to", like "allowing to", is improper
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
Diffstat (limited to 'doc/refman/RefMan-ext.tex')
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 8a5e8bb07..c4163b3b0 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -14,7 +14,7 @@ records as is done in many programming languages. Its syntax is described on Figure~\ref{record-syntax}. In fact, the \verb+Record+ macro is more general than the usual record types, since it allows also for ``manifest'' expressions. In this sense, the \verb+Record+ -construction allows to define ``signatures''. +construction allows defining ``signatures''. \begin{figure}[h] \begin{centerframe} @@ -208,7 +208,7 @@ Record point := { x : nat; y : nat }. Definition a := Build_point 5 3. \end{coq_example} -The following syntax allows to create objects by using named fields. The +The following syntax allows creating objects by using named fields. The fields do not have to be in any particular order, nor do they have to be all present if the missing ones can be inferred or prompted for (see Section~\ref{Program}). @@ -859,8 +859,8 @@ subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independe \index{Sections} \label{Section}} -The sectioning mechanism allows to organize a proof in structured -sections. Then local declarations become available (see +The sectioning mechanism can be used to to organize a proof in +structured sections. Then local declarations become available (see Section~\ref{Basic-definitions}). \subsection{\tt Section {\ident}\comindex{Section}} |