aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2018-04-24 11:59:48 +0200
committerThéo Zimmermann2018-05-05 11:54:02 +0200
commit7a569dfe04e62a97780c7f5f9e4f225b82c8f96a (patch)
tree05a4e730e33599f77cbe916e8ad12ded91b9cf8b
parentb9b2af0e19f13baae9b24aa3e11fb40ddf4fcb18 (diff)
[sphinx] Backport fix of typo.
(cf. 6131f89f6b91c45e641dd877df8719fa77987453)
-rw-r--r--doc/sphinx/proof-engine/proof-handling.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 86c94bab36..f62e956697 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -326,7 +326,7 @@ last ``Focus`` command.
.. cmd:: Unfocused.
-Succeeds if the proof is fully unfocused, fails is there are some
+Succeeds if the proof is fully unfocused, fails if there are some
goals out of focus.
.. _curly-braces: