Add some markers of origin.

7 files changed, 20 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
 ---------------------------------
 
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index d97c98da9c..87c9b96a84 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -14,6 +14,8 @@ of another, complementary, use of canonical structures: advanced proof search.
 This latter papers also presents many techniques one can employ to tune the
 inference of canonical structures.
 
+ .. extracted from implicit arguments section
+
 .. _canonical-structure-declaration:
 
 Declaraction of canonical structures
diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst
index 8dc5b99c4d..7635441c24 100644
--- a/doc/sphinx/language/extensions/evars.rst
+++ b/doc/sphinx/language/extensions/evars.rst
@@ -1,3 +1,5 @@
+.. extracted from Gallina extensions chapter
+
 .. _existential-variables:
 
 Existential variables
@@ -62,6 +64,8 @@ the syntax :n:`?[@ident]`. This is useful when the existential
 variable needs to be explicitly handled later in the script (e.g.
 with a named-goal selector, see :ref:`goal-selectors`).
 
+.. extracted from Gallina chapter
+
 .. index:: _
 
 Inferable subterms
@@ -71,6 +75,8 @@ Expressions often contain redundant pieces of information. Subterms that can be
 automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will
 guess the missing piece of information.
 
+.. extracted from Gallina extensions chapter
+
 .. _explicit-display-existentials:
 
 Explicit displaying of existential instances for pretty-printing
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index c5452d4590..b83e11e253 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -9,6 +9,8 @@ This section describes the full form of pattern matching in |Coq| terms.
 
 .. |rhs| replace:: right hand sides
 
+ .. extracted from Gallina extensions chapter
+
 Variants and extensions of :g:`match`
 -------------------------------------
 
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
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
 --------------------