aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-24 11:59:48 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-05 11:54:02 +0200
commit7a569dfe04e62a97780c7f5f9e4f225b82c8f96a (patch)
tree05a4e730e33599f77cbe916e8ad12ded91b9cf8b /doc
parentb9b2af0e19f13baae9b24aa3e11fb40ddf4fcb18 (diff)
[sphinx] Backport fix of typo.
Diffstat (limited to 'doc')
-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 86c94bab3..f62e95669 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: