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/user-extensions/syntax-extensions.rst | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'doc/sphinx/user-extensions')

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index e49073f593..8d1d46676c 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1383,6 +1383,8 @@ Abbreviations
    exception, if the right-hand side is just of the form :n:`@@qualid`,
    this conventionally stops the inheritance of implicit arguments.
 
+.. extracted from Gallina chapter
+
 Numerals and strings
 --------------------
 
-- 
cgit v1.2.3