diff options
Diffstat (limited to 'doc/sphinx/language/core')
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/modules.rst | 4 |
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 --------------------------------- |