From 4b7bdb46f8cc443ed82c0db51367130980a38974 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 9 May 2018 20:31:26 +0200
Subject: Clarify that the description of coqtop does not reflect all user
 interfaces.

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

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 45ee52b1e0..ec83f0e3e9 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -8,12 +8,13 @@
 In |Coq|’s proof editing mode all top-level commands documented in
 Chapter :ref:`vernacularcommands` remain available and the user has access to specialized
 commands dealing with proof development pragmas documented in this
-section. He can also use some other specialized commands called
+section. They can also use some other specialized commands called
 *tactics*. They are the very tools allowing the user to deal with
 logical reasoning. They are documented in Chapter :ref:`tactics`.
-When switching in editing proof mode, the prompt ``Coq <`` is changed into
-``ident <`` where ``ident`` is the declared name of the theorem currently
-edited.
+
+Coq user interfaces usually have a way of marking whether the user has
+switched to proof editing mode. For instance, in coqtop the prompt ``Coq <``   is changed into
+:n:`@ident <`   where :token:`ident` is the declared name of the theorem currently edited.
 
 At each stage of a proof development, one has a list of goals to
 prove. Initially, the list consists only in the theorem itself. After
-- 
cgit v1.2.3