aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Sam Pablo Kuper <sampablokuper@riseup.net>2017-08-01 13:10:14 +0100
committerGravatar Sam Pablo Kuper <sampablokuper@riseup.net>2017-08-01 13:10:14 +0100
commit8f0e4fbc634230d89bb710547bbb50a7f959d74b (patch)
tree007540028973961d81bca2ff24c39a63f1a01b8c /doc
parenta648f4ce7559fea0e4c269c776e654dea316a3b9 (diff)
Improve style slightly
per @aspiwack's comments in [this pull request review](https://github.com/coq/coq/pull/940).
Diffstat (limited to 'doc')
-rw-r--r--doc/tutorial/Tutorial.tex4
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