diff options
| author |  Sam Pablo Kuper <sampablokuper@riseup.net> | 2017-08-01 13:10:14 +0100 |
|---|---|---|
| committer | Sam Pablo Kuper <sampablokuper@riseup.net> | 2017-08-01 13:10:14 +0100 |
| commit | 8f0e4fbc634230d89bb710547bbb50a7f959d74b (patch) | |
| tree | 007540028973961d81bca2ff24c39a63f1a01b8c | |
| parent | a648f4ce7559fea0e4c269c776e654dea316a3b9 (diff) | |
Improve style slightly
per @aspiwack's comments in [this pull request
review](https://github.com/coq/coq/pull/940).
| -rw-r--r-- | doc/tutorial/Tutorial.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 17a132ea1..77ce8574f 100644 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -289,7 +289,7 @@ apply H. We are now in the situation where we have two judgments as conjectures that remain to be proved. Only the first is listed in full, for the others the system displays only the corresponding subgoal, without its -local hypotheses list. \verb:apply: has kept the local +local hypotheses list. Note that \verb:apply: has kept the local hypotheses of its father judgment, which are still available for the judgments it generated. @@ -666,7 +666,7 @@ Lemma refl_if : forall x : D, (exists y, R x y) -> R x x. The hypotheses that are local to the currently opened sections are listed as local hypotheses to the current goals. -The rationale for this is that these hypotheses are going to be discharged, as +That is because these hypotheses are going to be discharged, as we shall see, when we shall close the corresponding sections. Note the functional syntax for existential quantification. The existential |