From 26cd7d093822556fc919dc7e27cac0196f564fc2 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 14 May 2020 12:47:26 +0200
Subject: Add some markers of origin.

---
 doc/sphinx/proof-engine/vernacular-commands.rst | 2 ++
 1 file changed, 2 insertions(+)

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

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
-- 
cgit v1.2.3