From 3b8252d8990e715e5954812dffd0a5986cbb6012 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 4 Oct 2020 21:51:00 +0200
Subject: Documenting option Set Printing Goal Name.

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

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index f90ebadb3a..6c94baf959 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -858,6 +858,11 @@ Controlling the effect of proof editing commands
    proved before starting the previous proof) and Coq will switch back to the
    proof of the previous assertion.
 
+.. flag:: Printing Goal Names
+
+   When turned on, the name of the goal is printed in interactive
+   proof mode, which can be useful in cases of cross references
+   between goals.
 
 Controlling memory usage
 ------------------------
-- 
cgit v1.2.3