From 42ee49454a134896af4496fb9a4c9e3ae9a3f4df Mon Sep 17 00:00:00 2001
From: Sam Pablo Kuper
Date: Sun, 21 Oct 2018 19:00:53 +0100
Subject: Fix formatting. Use standard if..then grammar.

---
 doc/sphinx/proof-engine/proof-handling.rst | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index c802f44ac1..741f9fe5b0 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -144,8 +144,9 @@ list of assertion commands is given in :ref:`Assertions`. The command
    the proof is a subset of the declared one.
 
    The set of declared variables is closed under type dependency. For
-   example if ``T`` is variable and a is a variable of type ``T``, the commands
-   ``Proof using a`` and ``Proof using T a`` are actually equivalent.
+   example, if ``T`` is a variable and ``a`` is a variable of type
+   ``T``, then the commands ``Proof using a`` and ``Proof using T a``
+   are equivalent.
 
    .. cmdv:: Proof using {+ @ident } with @tactic
 
-- 
cgit v1.2.3