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/language/core/inductive.rst | 2 ++
 doc/sphinx/language/core/modules.rst   | 4 ++++
 2 files changed, 6 insertions(+)

(limited to 'doc/sphinx/language/core')

diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 53c8cd4701..4cdfba146a 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -508,6 +508,8 @@ constructions.
          | cons t f' => (tree_size t + forest_size f')
          end.
 
+.. extracted from CIC chapter
+
 .. _inductive-definitions:
 
 Theory of inductive definitions
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index b06dd2f1ab..29e703c223 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -50,6 +50,8 @@ A module type abbreviation is written :math:`\ModType{Y}{S}`,
 where :math:`Y` is an identifier and :math:`S` is any structure
 expression .
 
+.. extracted from Gallina extensions chapter
+
 Using modules
 -------------
 
@@ -852,6 +854,8 @@ and :math:`Γ_C` is :math:`[c_1 :C_1 ;…;c_n :C_n ]`.
    --------------------------
    E[] ⊢ p.c_i \triangleright_δ p'.c_i
 
+.. extracted from Gallina extensions chapter
+
 Libraries and qualified names
 ---------------------------------
 
-- 
cgit v1.2.3