From b1846e859091e24db1210be53f9193aa3aedb4d9 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 12 Sep 2020 20:54:22 -0700
Subject: Convert auto chapter to prodn

---
 doc/sphinx/language/core/inductive.rst | 5 ++---
 doc/sphinx/language/core/modules.rst   | 3 ++-
 doc/sphinx/language/core/sections.rst  | 3 ++-
 3 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'doc/sphinx/language')

diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 251b5e4955..9fda2ab1fa 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -8,14 +8,13 @@ Inductive types
 
 .. cmd:: Inductive @inductive_definition {* with @inductive_definition }
 
-   .. insertprodn inductive_definition cumul_ident_decl
+   .. insertprodn inductive_definition constructor
 
    .. prodn::
-      inductive_definition ::= {? > } @cumul_ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
+      inductive_definition ::= {? > } @ident {? @cumul_univ_decl } {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
       constructors_or_record ::= {? %| } {+| @constructor }
       | {? @ident } %{ {*; @record_field } {? ; } %}
       constructor ::= @ident {* @binder } {? @of_type }
-      cumul_ident_decl ::= @ident {? @cumul_univ_decl }
 
    This command defines one or more
    inductive types and its constructors.  Coq generates destructors
diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index 54252689e1..6d96e15202 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -155,7 +155,8 @@ are now available through the dot notation.
   #. Interactive modules and module types can be nested.
   #. Interactive modules and module types can't be defined inside of :ref:`sections<section-mechanism>`.
      Sections can be defined inside of interactive modules and module types.
-  #. Hints and notations (:cmd:`Hint` and :cmd:`Notation` commands) can also appear inside interactive
+  #. Hints and notations (the :ref:`Hint <creating_hints>` and :cmd:`Notation`
+     commands) can also appear inside interactive
      modules and module types. Note that with module definitions like:
 
      :n:`Module @ident__1 : @module_type := @ident__2.`
diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst
index df50dbafe3..75389bb259 100644
--- a/doc/sphinx/language/core/sections.rst
+++ b/doc/sphinx/language/core/sections.rst
@@ -69,7 +69,8 @@ Sections create local contexts which can be shared across multiple definitions.
        :undocumented:
 
 .. note::
-   Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which
+   Most commands, such as the :ref:`Hint <creating_hints>` commands,
+   :cmd:`Notation` and option management commands that
    appear inside a section are canceled when the section is closed.
 
 .. cmd:: Let @ident_decl @def_body
-- 
cgit v1.2.3