Convert misc chapters to prodn

6 files changed, 37 insertions, 15 deletions

diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index 6cdc272fd4..a38282d41a 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -141,8 +141,8 @@ has type :n:`@type`.
       of_type ::= {| : | :> } @type
 
    These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in
-   the global context. The fact asserted by the :n:`@type` (or, equivalently, the existence
-   of an object of this type) is accepted as a postulate.
+   the global context. The fact asserted by :n:`@type` (or, equivalently, the existence
+   of an object of this type) is accepted as a postulate.  They accept the :attr:`program` attribute.
 
    :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms
    are equivalent.  They can take the :attr:`local` :term:`attribute`,
@@ -155,6 +155,10 @@ has type :n:`@type`.
    is closed, the :n:`@ident`\(s) become undefined and every object depending on them will be explicitly
    parameterized (i.e., the variables are *discharged*).  See Section :ref:`section-mechanism`.
 
+   :n:`:>`
+     If specified, :token:`ident_decl` is automatically
+     declared as a coercion to the class of its type.  See :ref:`coercions`.
+
    The :n:`Inline` clause is only relevant inside functors.  See :cmd:`Module`.
 
 .. example:: Simple assumptions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 3cc3fe231a..321199f05f 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -325,10 +325,10 @@ rest of the |Coq| manual: :term:`terms <term>` and :term:`types
      boldface label "Command:".  Commands are listed in the
      :ref:`command_index`.  Example:
 
-     .. cmd:: Comments {* @string }
+     .. cmd:: Comments {* {| @one_term | @string | @natural } }
 
-        This command prints "Comments ok" and does not change anything
-        to the state of the document.
+        Prints "Comments ok" and does not change
+        the state of the document.
 
    tactic
 
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 592b16a72f..8d67a3cf40 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -87,7 +87,7 @@ Section :ref:`typing-rules`.
    computation on :n:`@term`.
 
    These commands also support the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`program` and
+   :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`) and
    :attr:`canonical` attributes.
 
    If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode.
@@ -140,6 +140,8 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and
    the theorem is bound to the name :n:`@ident` in the environment.
 
+   These commands accept the :attr:`program` attribute.  See :ref:`program_lemma`.
+
    Forms using the :n:`with` clause are useful for theorems that are proved by simultaneous induction
    over a mutually inductive assumption, or that assert mutually dependent
    statements in some mutual co-inductive type. It is equivalent to
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 0b18c9dcf1..122b0f5dfb 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -361,7 +361,11 @@ syntax: :n:`let fix @ident {* @binder } := @term in` stands for
 
 Some options of :n:`@fixannot` are only supported in specific constructs.  :n:`fix` and :n:`let fix`
 only support the :n:`struct` option, while :n:`wf` and :n:`measure` are only supported in
-commands such as :cmd:`Function` and :cmd:`Program Fixpoint`.
+commands such as :cmd:`Fixpoint` (with the :attr:`program` attribute) and :cmd:`Function`.
+
+.. todo explanation of struct: see text above at the Fixpoint command, also
+   see https://github.com/coq/coq/pull/12936#discussion_r510716268 and above.
+   Consider whether to move the grammar for fixannot elsewhere
 
 .. _Fixpoint:
 
@@ -379,7 +383,7 @@ constructions.
    .. prodn::
       fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations }
 
-   This command allows defining functions by pattern matching over inductive
+   Allows defining functions by pattern matching over inductive
    objects using a fixed point construction. The meaning of this declaration is
    to define :n:`@ident` as a recursive function with arguments specified by
    the :n:`@binder`\s such that :n:`@ident` applied to arguments
@@ -388,6 +392,8 @@ constructions.
    consequently :n:`forall {* @binder }, @type` and its value is equivalent
    to :n:`fun {* @binder } => @term`.
 
+   This command accepts the :attr:`program` attribute.
+
    To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical
    constraints on a special argument called the decreasing argument. They
    are needed to ensure that the :cmd:`Fixpoint` definition always terminates.
@@ -399,7 +405,7 @@ constructions.
    that satisfies the decreasing condition.
 
    :cmd:`Fixpoint` without the :attr:`program` attribute does not support the
-   :n:`wf` or :n:`measure` clauses of :n:`@fixannot`.
+   :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. See :ref:`program_fixpoint`.
 
    The :n:`with` clause allows simultaneously defining several mutual fixpoints.
    It is especially useful when defining functions over mutually defined
diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst
index b2099b8636..e6df3ee9f5 100644
--- a/doc/sphinx/language/core/records.rst
+++ b/doc/sphinx/language/core/records.rst
@@ -18,7 +18,7 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
    .. insertprodn record_definition field_def
 
    .. prodn::
-      record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } {? ; } %} {? @decl_notations }
+      record_definition ::= {? > } @ident_decl {* @binder } {? : @sort } {? := {? @ident } %{ {*; @record_field } {? ; } %} }
       record_field ::= {* #[ {*, @attribute } ] } @name {? @field_body } {? %| @natural } {? @decl_notations }
       field_body ::= {* @binder } @of_type
       | {* @binder } @of_type := @term
@@ -26,19 +26,28 @@ expressions. In this sense, the :cmd:`Record` construction allows defining
       term_record ::= %{%| {*; @field_def } {? ; } %|%}
       field_def ::= @qualid {* @binder } := @term
 
-
    Each :n:`@record_definition` defines a record named by :n:`@ident_decl`.
    The constructor name is given by :n:`@ident`.
    If the constructor name is not specified, then the default name :n:`Build_@ident` is used,
    where :n:`@ident` is the record name.
 
-   If :n:`@type` is
-   omitted, the default type is :math:`\Type`. The identifiers inside the brackets are the field names.
-   The type of each field :n:`@ident` is :n:`forall {* @binder }, @type`.
+   If :token:`sort` is omitted, the default sort is Type.
    Notice that the type of an identifier can depend on a previously-given identifier. Thus the
    order of the fields is important. :n:`@binder` parameters may be applied to the record as a whole
    or to individual fields.
 
+   .. todo
+      "Record foo2:Prop := { a }." gives the error "Cannot infer this placeholder of type "Type",
+      while "Record foo2:Prop := { a:Type }." gives the output "foo2 is defined.
+      a cannot be defined because it is informative and foo2 is not."
+      Your thoughts?
+
+   :n:`{? > }`
+     If provided, the constructor name is automatically declared as
+     a coercion from the class of the last field type to the record name
+     (this may fail if the uniform inheritance condition is not
+     satisfied).  See :ref:`coercions`.
+
    Notations can be attached to fields using the :n:`@decl_notations` annotation.
 
    :cmd:`Record` and :cmd:`Structure` are synonyms.
@@ -76,7 +85,7 @@ Let us now see the work done by the ``Record`` macro. First the macro
 generates a variant type definition with just one constructor:
 :n:`Variant @ident {* @binder } : @sort := @ident__0 {* @binder }`.
 
-To build an object of type :token:`ident`, one should provide the constructor
+To build an object of type :token:`ident`, provide the constructor
 :n:`@ident__0` with the appropriate number of terms filling the fields of the record.
 
 .. example::
diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst
index 2904250e41..645986be9c 100644
--- a/doc/sphinx/language/core/variants.rst
+++ b/doc/sphinx/language/core/variants.rst
@@ -29,6 +29,7 @@ Private (matching) inductive types
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 .. attr:: private(matching)
+   :name: private(matching); Private
 
    This attribute can be used to forbid the use of the :g:`match`
    construct on objects of this inductive type outside of the module