Add some markers of origin.

2 files changed, 6 insertions, 0 deletions

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
 ---------------------------------