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-coi.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-coi.tex')
| -rw-r--r-- | doc/refman/RefMan-coi.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex index d75b9eb93..4ef5818aa 100644 --- a/doc/refman/RefMan-coi.tex +++ b/doc/refman/RefMan-coi.tex @@ -286,7 +286,7 @@ Reset eqproof. \noindent Instead of giving an explicit definition, we can use the proof editor of Coq to help us in the construction of the proof. -A tactic \verb!Cofix! allows to place a \verb!CoFixpoint! definition +A tactic \verb!Cofix! allows placing a \verb!CoFixpoint! definition inside a proof. This tactic introduces a variable in the context which has the same type as the current goal, and its application stands @@ -331,8 +331,8 @@ with the tactic \verb!Cofix!. Remark that once it has been used the application of tactics performing automatic proof search in the environment (like for example \verb!Auto!) could introduce unguarded recursive calls in the proof. -The command \verb!Guarded! allows to verify -if the guarded condition has been violated +The command \verb!Guarded! verifies +that the guarded condition has been not violated during the construction of the proof. This command can be applied even if the proof term is not complete. |