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-gal.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-gal.tex')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 2f128abaa..b8e715c76 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -3,7 +3,7 @@ \label{BNF-syntax} % Used referred to as a chapter label This chapter describes \gallina, the specification language of {\Coq}. -It allows to develop mathematical theories and to prove specifications +It allows developing mathematical theories and to prove specifications of programs. The theories are built from axioms, hypotheses, parameters, lemmas, theorems and definitions of constants, functions, predicates and sets. The syntax of logical objects involved in @@ -989,7 +989,7 @@ Check nat_ind. This is the well known structural induction principle over natural numbers, i.e. the second-order form of Peano's induction principle. -It allows to prove some universal property of natural numbers ({\tt +It allows proving some universal property of natural numbers ({\tt forall n:nat, P n}) by induction on {\tt n}. The types of {\tt nat\_rec} and {\tt nat\_rect} are similar, except @@ -1327,7 +1327,7 @@ constructions. The command: \ident$_0$ {\tt \}} : type$_0$ := \term$_0$ \comindex{Fixpoint}\label{Fixpoint}} \end{center} -allows to define functions by pattern-matching over inductive objects +allows defining functions by pattern-matching over inductive objects using a fixed point construction. The meaning of this declaration is to define {\it ident} a recursive function with arguments specified by the binders in {\params} such @@ -1610,7 +1610,7 @@ The command can be used also with {\tt Lemma}, \item {\tt Definition {\ident} \zeroone{\binders} : {\type}.} -This allows to define a term of type {\type} using the proof editing mode. It +This allows defining a term of type {\type} using the proof editing mode. It behaves as {\tt Theorem} but is intended to be used in conjunction with {\tt Defined} (see \ref{Defined}) in order to define a constant of which the computational behavior is relevant. |