aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/proof-engine')
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 2ba41ba9e5..031abbe15c 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -747,6 +747,8 @@ Controlling display
after each tactic. The information is used by the Prooftree tool in Proof
General. (https://askra.de/software/prooftree)
+.. extracted from Gallina extensions chapter
+
.. _printing_constructions_full:
Printing constructions in full