aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
diff options
context:
space:
mode:
authorThéo Zimmermann2020-05-14 12:47:26 +0200
committerThéo Zimmermann2020-05-14 12:47:26 +0200
commit26cd7d093822556fc919dc7e27cac0196f564fc2 (patch)
tree51bacd2d39daf9da9698918f6aa151fa8c676640 /doc/sphinx/proof-engine
parent95c4fc791b1eda5357855f706dfdb4c050d6c28e (diff)
Add some markers of origin.
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