Document the Fast Name Printing option.

1 files changed, 14 insertions, 0 deletions

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 3e8dd25ee0..e207a072cc 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -510,6 +510,20 @@ Requests to the environment
 
 .. seealso:: Section :ref:`locating-notations`
 
+.. _printing-flags:
+
+Printing flags
+-------------------------------
+
+.. flag:: Fast Name Printing
+
+   When turned on, |Coq| uses an asymptotically faster algorithm for the
+   generation of unambiguous names of bound variables while printing terms.
+   While faster, it is also less clever and results in a typically less elegant
+   display, e.g. it will generate more names rather than reusing certain names
+   across subterms. This flag is not enabled by default, because as Ltac
+   observes bound names, turning it on can break existing proof scripts.
+
 
 .. _loading-files: