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/Classes.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/Classes.tex')
| -rw-r--r-- | doc/refman/Classes.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index ea1ae02bc..869ba971c 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -403,7 +403,7 @@ This is equivalent to {\tt Hint Transparent,Opaque} {\ident} {\tt: typeclass\_in \comindex{Typeclasses eauto} \label{TypeclassesEauto} -This commands allows to customize the type class resolution tactic, +This command allows customization of the type class resolution tactic, based on a variant of eauto. The flags semantics are: \begin{itemize} \item {\tt debug} In debug mode, the trace of successfully applied |