Extract functions and assumptions.

1 files changed, 8 insertions, 1274 deletions

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 353bed1b3d..9943e0aa76 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1,111 +1,5 @@
-.. _gallinaspecificationlanguage:
-
-------------------------------------
- The Gallina specification language
-------------------------------------
-
-This chapter describes Gallina, the specification language of Coq. It allows
-developing mathematical theories and to prove specifications of programs. The
-theories are built from axioms, hypotheses, parameters, lemmas, theorems and
-definitions of constants, functions, predicates and sets.
-
-.. _term:
-
-Terms
-=====
-
-.. _gallina-identifiers:
-
-Qualified identifiers and simple identifiers
---------------------------------------------
-
-.. insertprodn qualid field_ident
-
-.. prodn::
-   qualid ::= @ident {* @field_ident }
-   field_ident ::= .@ident
-
-*Qualified identifiers* (:n:`@qualid`) denote *global constants*
-(definitions, lemmas, theorems, remarks or facts), *global variables*
-(parameters or axioms), *inductive types* or *constructors of inductive
-types*. *Simple identifiers* (or shortly :n:`@ident`) are a syntactic subset
-of qualified identifiers. Identifiers may also denote *local variables*,
-while qualified identifiers do not.
-
-Field identifiers, written :n:`@field_ident`, are identifiers prefixed by
-`.` (dot) with no blank between the dot and the identifier.
-
-
-Numerals and strings
---------------------
-
-.. insertprodn primitive_notations primitive_notations
-
-.. prodn::
-   primitive_notations ::= @numeral
-   | @string
-
-Numerals and strings have no predefined semantics in the calculus. They are
-merely notations that can be bound to objects through the notation mechanism
-(see Chapter :ref:`syntax-extensions-and-notation-scopes` for details).
-Initially, numerals are bound to Peano’s representation of natural
-numbers (see :ref:`datatypes`).
-
-.. note::
-
-   Negative integers are not at the same level as :n:`@num`, for this
-   would make precedence unnatural.
-
-.. index::
-   single: Set (sort)
-   single: SProp
-   single: Prop
-   single: Type
-
-Sorts
------
-
-.. insertprodn sort univ_constraint
-
-.. prodn::
-   sort ::= Set
-   | Prop
-   | SProp
-   | Type
-   | Type @%{ _ %}
-   | Type @%{ @universe %}
-   universe ::= max ( {+, @universe_expr } )
-   | @universe_expr
-   universe_expr ::= @universe_name {? + @num }
-   universe_name ::= @qualid
-   | Set
-   | Prop
-   univ_annot ::= @%{ {* @universe_level } %}
-   universe_level ::= Set
-   | Prop
-   | Type
-   | _
-   | @qualid
-   univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %}
-   univ_constraint ::= @universe_name {| < | = | <= } @universe_name
-
-There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set`  and :g:`Type`.
-
--  :g:`SProp` is the universe of *definitionally irrelevant
-   propositions* (also called *strict propositions*).
-
--  :g:`Prop` is the universe of *logical propositions*. The logical propositions
-   themselves are typing the proofs. We denote propositions by :n:`@form`.
-   This constitutes a semantic subclass of the syntactic class :n:`@term`.
-
--  :g:`Set` is the universe of *program types* or *specifications*. The
-   specifications themselves are typing the programs. We denote
-   specifications by :n:`@specif`. This constitutes a semantic subclass of
-   the syntactic class :n:`@term`.
-
--  :g:`Type` is the type of sorts.
-
-More on sorts can be found in Section :ref:`sorts`.
+Functions and assumptions
+=========================
 
 .. _binders:
 
@@ -155,6 +49,12 @@ the case of a single sequence of bindings sharing the same type (e.g.:
 Abstractions: fun
 -----------------
 
+.. insertprodn term_forall_or_fun term_forall_or_fun
+
+.. prodn::
+   term_forall_or_fun ::= forall @open_binders , @term
+   | fun @open_binders => @term
+
 The expression :n:`fun @ident : @type => @term` defines the
 *abstraction* of the variable :n:`@ident`, of type :n:`@type`, over the term
 :n:`@term`. It denotes a function of the variable :n:`@ident` that evaluates to
@@ -174,12 +74,6 @@ Section :ref:`let-in`).
 Products: forall
 ----------------
 
-.. insertprodn term_forall_or_fun term_forall_or_fun
-
-.. prodn::
-   term_forall_or_fun ::= forall @open_binders , @term
-   | fun @open_binders => @term
-
 The expression :n:`forall @ident : @type, @term` denotes the
 *product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`.
 As for abstractions, :g:`forall` is followed by a binder list, and products
@@ -220,256 +114,6 @@ The notation :n:`(@ident := @term)` for arguments is used for making
 explicit the value of implicit arguments (see
 Section :ref:`explicit-applications`).
 
-.. index::
-   single: ... : ... (type cast)
-   single: ... <: ...
-   single: ... <<: ...
-
-Type cast
----------
-
-.. insertprodn term_cast term_cast
-
-.. prodn::
-   term_cast ::= @term10 <: @term
-   | @term10 <<: @term
-   | @term10 : @term
-   | @term10 :>
-
-The expression :n:`@term : @type` is a type cast expression. It enforces
-the type of :n:`@term` to be :n:`@type`.
-
-:n:`@term <: @type` locally sets up the virtual machine for checking that
-:n:`@term` has type :n:`@type`.
-
-:n:`@term <<: @type` uses native compilation for checking that :n:`@term`
-has type :n:`@type`.
-
-.. index:: _
-
-Inferable subterms
-------------------
-
-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.
-
-.. index:: let ... := ... (term)
-
-.. _let-in:
-
-Let-in definitions
-------------------
-
-.. insertprodn term_let term_let
-
-.. prodn::
-   term_let ::= let @name {? : @type } := @term in @term
-   | let @name {+ @binder } {? : @type } := @term in @term
-   | let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term
-   | let ' @pattern := @term {? return @term100 } in @term
-   | let ' @pattern in @pattern := @term return @term100 in @term
-
-:n:`let @ident := @term in @term’`
-denotes the local binding of :n:`@term` to the variable
-:n:`@ident` in :n:`@term`’. There is a syntactic sugar for let-in
-definition of functions: :n:`let @ident {+ @binder} := @term in @term’`
-stands for :n:`let @ident := fun {+ @binder} => @term in @term’`.
-
-.. index:: match ... with ...
-
-Definition by cases: match
---------------------------
-
-.. insertprodn term_match pattern0
-
-.. prodn::
-   term_match ::= match {+, @case_item } {? return @term100 } with {? %| } {*| @eqn } end
-   case_item ::= @term100 {? as @name } {? in @pattern }
-   eqn ::= {+| {+, @pattern } } => @term
-   pattern ::= @pattern10 : @term
-   | @pattern10
-   pattern10 ::= @pattern1 as @name
-   | @pattern1 {* @pattern1 }
-   | @ @qualid {* @pattern1 }
-   pattern1 ::= @pattern0 % @scope_key
-   | @pattern0
-   pattern0 ::= @qualid
-   | %{%| {* @qualid := @pattern } %|%}
-   | _
-   | ( {+| @pattern } )
-   | @numeral
-   | @string
-
-Objects of inductive types can be destructured by a case-analysis
-construction called *pattern matching* expression. A pattern matching
-expression is used to analyze the structure of an inductive object and
-to apply specific treatments accordingly.
-
-This paragraph describes the basic form of pattern matching. See
-Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description
-of the general form. The basic form of pattern matching is characterized
-by a single :n:`@case_item` expression, an :n:`@eqn` restricted to a
-single :n:`@pattern` and :n:`@pattern` restricted to the form
-:n:`@qualid {* @ident}`.
-
-The expression
-:n:`match @term {? return @term100 } with {+| @pattern__i => @term__i } end` denotes a
-*pattern matching* over the term :n:`@term` (expected to be
-of an inductive type :math:`I`). The :n:`@term__i`
-are the *branches* of the pattern matching
-expression. Each :n:`@pattern__i` has the form :n:`@qualid @ident`
-where :n:`@qualid` must denote a constructor. There should be
-exactly one branch for every constructor of :math:`I`.
-
-The :n:`return @term100` clause gives the type returned by the whole match
-expression. There are several cases. In the *non dependent* case, all
-branches have the same type, and the :n:`return @term100` specifies that type.
-In this case, :n:`return @term100` can usually be omitted as it can be
-inferred from the type of the branches [1]_.
-
-In the *dependent* case, there are three subcases. In the first subcase,
-the type in each branch may depend on the exact value being matched in
-the branch. In this case, the whole pattern matching itself depends on
-the term being matched. This dependency of the term being matched in the
-return type is expressed with an :n:`@ident` clause where :n:`@ident`
-is dependent in the return type. For instance, in the following example:
-
-.. coqtop:: in
-
-   Inductive bool : Type := true : bool | false : bool.
-   Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x.
-   Inductive or (A:Prop) (B:Prop) : Prop :=
-     | or_introl : A -> or A B
-     | or_intror : B -> or A B.
-
-   Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) :=
-     match b as x return or (eq bool x true) (eq bool x false) with
-     | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true)
-     | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false)
-     end.
-
-the branches have respective types ":g:`or (eq bool true true) (eq bool true false)`"
-and ":g:`or (eq bool false true) (eq bool false false)`" while the whole
-pattern matching expression has type ":g:`or (eq bool b true) (eq bool b false)`",
-the identifier :g:`b` being used to represent the dependency.
-
-.. note::
-
-   When the term being matched is a variable, the ``as`` clause can be
-   omitted and the term being matched can serve itself as binding name in
-   the return type. For instance, the following alternative definition is
-   accepted and has the same meaning as the previous one.
-
-   .. coqtop:: none
-
-      Reset bool_case.
-
-   .. coqtop:: in
-
-      Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false) :=
-      match b return or (eq bool b true) (eq bool b false) with
-      | true => or_introl (eq bool true true) (eq bool true false) (eq_refl bool true)
-      | false => or_intror (eq bool false true) (eq bool false false) (eq_refl bool false)
-      end.
-
-The second subcase is only relevant for annotated inductive types such
-as the equality predicate (see Section :ref:`coq-equality`),
-the order predicate on natural numbers or the type of lists of a given
-length (see Section :ref:`matching-dependent`). In this configuration, the
-type of each branch can depend on the type dependencies specific to the
-branch and the whole pattern matching expression has a type determined
-by the specific dependencies in the type of the term being matched. This
-dependency of the return type in the annotations of the inductive type
-is expressed with a clause in the form
-:n:`in @qualid {+ _ } {+ @pattern }`, where
-
--  :n:`@qualid` is the inductive type of the term being matched;
-
--  the holes :n:`_` match the parameters of the inductive type: the
-   return type is not dependent on them.
-
--  each :n:`@pattern` matches the annotations of the
-   inductive type: the return type is dependent on them
-
--  in the basic case which we describe below, each :n:`@pattern`
-   is a name :n:`@ident`; see :ref:`match-in-patterns` for the
-   general case
-
-For instance, in the following example:
-
-.. coqtop:: in
-
-   Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x :=
-   match H in eq _ _ z return eq A z x with
-   | eq_refl _ _ => eq_refl A x
-   end.
-
-the type of the branch is :g:`eq A x x` because the third argument of
-:g:`eq` is :g:`x` in the type of the pattern :g:`eq_refl`. On the contrary, the
-type of the whole pattern matching expression has type :g:`eq A y x` because the
-third argument of eq is y in the type of H. This dependency of the case analysis
-in the third argument of :g:`eq` is expressed by the identifier :g:`z` in the
-return type.
-
-Finally, the third subcase is a combination of the first and second
-subcase. In particular, it only applies to pattern matching on terms in
-a type with annotations. For this third subcase, both the clauses ``as`` and
-``in`` are available.
-
-There are specific notations for case analysis on types with one or two
-constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see
-Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`).
-
-.. index::
-   single: fix
-   single: cofix
-
-Recursive and co-recursive functions: fix and cofix
----------------------------------------------------
-
-.. insertprodn term_fix fixannot
-
-.. prodn::
-   term_fix ::= let fix @fix_body in @term
-   | fix @fix_body {? {+ with @fix_body } for @ident }
-   fix_body ::= @ident {* @binder } {? @fixannot } {? : @type } := @term
-   fixannot ::= %{ struct @ident %}
-   | %{ wf @one_term @ident %}
-   | %{ measure @one_term {? @ident } {? @one_term } %}
-
-
-The expression ":n:`fix @ident__1 @binder__1 : @type__1 := @term__1 with … with @ident__n @binder__n : @type__n := @term__n for @ident__i`" denotes the
-:math:`i`-th component of a block of functions defined by mutual structural
-recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When
-:math:`n=1`, the ":n:`for @ident__i`" clause is omitted.
-
-The association of a single fixpoint and a local definition have a special
-syntax: :n:`let fix @ident {* @binder } := @term in` stands for
-:n:`let @ident := fix @ident {* @binder } := @term in`. The same applies for co-fixpoints.
-
-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`.
-
-.. insertprodn term_cofix cofix_body
-
-.. prodn::
-   term_cofix ::= let cofix @cofix_body in @term
-   | cofix @cofix_body {? {+ with @cofix_body } for @ident }
-   cofix_body ::= @ident {* @binder } {? : @type } := @term
-
-The expression
-":n:`cofix @ident__1 @binder__1 : @type__1 with … with @ident__n @binder__n : @type__n for @ident__i`"
-denotes the :math:`i`-th component of a block of terms defined by a mutual guarded
-co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When
-:math:`n=1`, the ":n:`for @ident__i`" clause is omitted.
-
-.. _vernacular:
-
-The Vernacular
-==============
-
 .. _gallina-assumptions:
 
 Assumptions
@@ -540,913 +184,3 @@ has type :n:`@type`.
    the assertion :n:`@type` is of sort :g:`Prop`), and to use the commands
    :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases
    (corresponding to the declaration of an abstract object of the given type).
-
-.. _gallina-definitions:
-
-Definitions
------------
-
-Definitions extend the environment with associations of names to terms.
-A definition can be seen as a way to give a meaning to a name or as a
-way to abbreviate a term. In any case, the name can later be replaced at
-any time by its definition.
-
-The operation of unfolding a name into its definition is called
-:math:`\delta`-conversion (see Section :ref:`delta-reduction`). A
-definition is accepted by the system if and only if the defined term is
-well-typed in the current context of the definition and if the name is
-not already used. The name defined by the definition is called a
-*constant* and the term it refers to is its *body*. A definition has a
-type which is the type of its body.
-
-A formal presentation of constants and environments is given in
-Section :ref:`typing-rules`.
-
-.. cmd:: {| Definition | Example } @ident_decl @def_body
-   :name: Definition; Example
-
-   .. insertprodn def_body def_body
-
-   .. prodn::
-      def_body ::= {* @binder } {? : @type } := {? @reduce } @term
-      | {* @binder } : @type
-
-   These commands bind :n:`@term` to the name :n:`@ident` in the environment,
-   provided that :n:`@term` is well-typed.  They can take the :attr:`local` :term:`attribute`,
-   which makes the defined :n:`@ident` accessible by :cmd:`Import` and its variants
-   only through their fully qualified names.
-   If :n:`@reduce` is present then :n:`@ident` is bound to the result of the specified
-   computation on :n:`@term`.
-
-   These commands also support the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`program` and
-   :attr:`canonical` attributes.
-
-   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
-   This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
-   In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
-   for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
-
-   The form :n:`Definition @ident : @type := @term` checks that the type of :n:`@term`
-   is definitionally equal to :n:`@type`, and registers :n:`@ident` as being of type
-   :n:`@type`, and bound to value :n:`@term`.
-
-   The form :n:`Definition @ident {* @binder } : @type := @term` is equivalent to
-   :n:`Definition @ident : forall {* @binder }, @type := fun {* @binder } => @term`.
-
-   .. seealso:: :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
-
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Definition)
-      :undocumented:
-
-   .. exn:: The term @term has type @type while it is expected to have type @type'.
-      :undocumented:
-
-.. _gallina-inductive-definitions:
-
-Inductive types
----------------
-
-.. cmd:: Inductive @inductive_definition {* with @inductive_definition }
-
-   .. insertprodn inductive_definition constructor
-
-   .. prodn::
-      inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations }
-      constructors_or_record ::= {? %| } {+| @constructor }
-      | {? @ident } %{ {*; @record_field } %}
-      constructor ::= @ident {* @binder } {? @of_type }
-
-   This command defines one or more
-   inductive types and its constructors.  Coq generates destructors
-   depending on the universe that the inductive type belongs to.
-
-   The destructors are named :n:`@ident`\ ``_rect``, :n:`@ident`\ ``_ind``,
-   :n:`@ident`\ ``_rec`` and :n:`@ident`\ ``_sind``, which
-   respectively correspond to elimination principles on :g:`Type`, :g:`Prop`,
-   :g:`Set` and :g:`SProp`.  The type of the destructors
-   expresses structural induction/recursion principles over objects of
-   type :n:`@ident`.  The constant :n:`@ident`\ ``_ind`` is always
-   generated, whereas :n:`@ident`\ ``_rec`` and :n:`@ident`\ ``_rect``
-   may be impossible to derive (for example, when :n:`@ident` is a
-   proposition).
-
-   This command supports the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`universes(template)`,
-   :attr:`universes(notemplate)`, :attr:`universes(cumulative)`,
-   :attr:`universes(noncumulative)` and :attr:`private(matching)`
-   attributes.
-
-   Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
-   The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked.
-   Each :n:`@ident` can be used independently thereafter.
-   See :ref:`mutually_inductive_types`.
-
-   If the entire inductive definition is parameterized with :n:`@binder`\s, the parameters correspond
-   to a local context in which the entire set of inductive declarations is interpreted.
-   For this reason, the parameters must be strictly the same for each inductive type.
-   See :ref:`parametrized-inductive-types`.
-
-   Constructor :n:`@ident`\s can come with :n:`@binder`\s, in which case
-   the actual type of the constructor is :n:`forall {* @binder }, @type`.
-
-   .. exn:: Non strictly positive occurrence of @ident in @type.
-
-      The types of the constructors have to satisfy a *positivity condition*
-      (see Section :ref:`positivity`). This condition ensures the soundness of
-      the inductive definition. The positivity checking can be disabled using
-      the :flag:`Positivity Checking` flag (see :ref:`controlling-typing-flags`).
-
-   .. exn:: The conclusion of @type is not valid; it must be built from @ident.
-
-      The conclusion of the type of the constructors must be the inductive type
-      :n:`@ident` being defined (or :n:`@ident` applied to arguments in
-      the case of annotated inductive types — cf. next section).
-
-The following subsections show examples of simple inductive types,
-simple annotated inductive types, simple parametric inductive types,
-mutually inductive types and private (matching) inductive types.
-
-.. _simple-inductive-types:
-
-Simple inductive types
-~~~~~~~~~~~~~~~~~~~~~~
-
-A simple inductive type belongs to a universe that is a simple :n:`@sort`.
-
-.. example::
-
-   The set of natural numbers is defined as:
-
-   .. coqtop:: reset all
-
-      Inductive nat : Set :=
-      | O : nat
-      | S : nat -> nat.
-
-   The type nat is defined as the least :g:`Set` containing :g:`O` and closed by
-   the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the
-   environment.
-
-   This definition generates four elimination principles:
-   :g:`nat_rect`, :g:`nat_ind`, :g:`nat_rec` and :g:`nat_sind`. The type of :g:`nat_ind` is:
-
-   .. coqtop:: all
-
-      Check nat_ind.
-
-   This is the well known structural induction principle over natural
-   numbers, i.e. the second-order form of Peano’s induction principle. It
-   allows proving universal properties of natural numbers (:g:`forall
-   n:nat, P n`) by induction on :g:`n`.
-
-   The types of :g:`nat_rect`, :g:`nat_rec` and :g:`nat_sind` are similar, except that they
-   apply to, respectively, :g:`(P:nat->Type)`, :g:`(P:nat->Set)` and :g:`(P:nat->SProp)`. They correspond to
-   primitive induction principles (allowing dependent types) respectively
-   over sorts ```Type``, ``Set`` and ``SProp``.
-
-In the case where inductive types don't have annotations (the next section
-gives an example of annotations), a constructor can be defined
-by giving the type of its arguments alone.
-
-.. example::
-
-   .. coqtop:: reset none
-
-      Reset nat.
-
-   .. coqtop:: in
-
-      Inductive nat : Set := O | S (_:nat).
-
-Simple annotated inductive types
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-In annotated inductive types, the universe where the inductive type
-is defined is no longer a simple :n:`@sort`, but what is called an arity,
-which is a type whose conclusion is a :n:`@sort`.
-
-.. example::
-
-   As an example of annotated inductive types, let us define the
-   :g:`even` predicate:
-
-   .. coqtop:: all
-
-      Inductive even : nat -> Prop :=
-      | even_0 : even O
-      | even_SS : forall n:nat, even n -> even (S (S n)).
-
-   The type :g:`nat->Prop` means that :g:`even` is a unary predicate (inductively
-   defined) over natural numbers. The type of its two constructors are the
-   defining clauses of the predicate :g:`even`. The type of :g:`even_ind` is:
-
-   .. coqtop:: all
-
-      Check even_ind.
-
-   From a mathematical point of view, this asserts that the natural numbers satisfying
-   the predicate :g:`even` are exactly in the smallest set of naturals satisfying the
-   clauses :g:`even_0` or :g:`even_SS`. This is why, when we want to prove any
-   predicate :g:`P` over elements of :g:`even`, it is enough to prove it for :g:`O`
-   and to prove that if any natural number :g:`n` satisfies :g:`P` its double
-   successor :g:`(S (S n))` satisfies also :g:`P`. This is analogous to the
-   structural induction principle we got for :g:`nat`.
-
-.. _parametrized-inductive-types:
-
-Parameterized inductive types
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-In the previous example, each constructor introduces a different
-instance of the predicate :g:`even`. In some cases, all the constructors
-introduce the same generic instance of the inductive definition, in
-which case, instead of an annotation, we use a context of parameters
-which are :n:`@binder`\s shared by all the constructors of the definition.
-
-Parameters differ from inductive type annotations in that the
-conclusion of each type of constructor invokes the inductive type with
-the same parameter values of its specification.
-
-.. example::
-
-   A typical example is the definition of polymorphic lists:
-
-   .. coqtop:: all
-
-      Inductive list (A:Set) : Set :=
-      | nil : list A
-      | cons : A -> list A -> list A.
-
-   In the type of :g:`nil` and :g:`cons`, we write ":g:`list A`" and not
-   just ":g:`list`". The constructors :g:`nil` and :g:`cons` have these types:
-
-   .. coqtop:: all
-
-      Check nil.
-      Check cons.
-
-   Observe that the destructors are also quantified with :g:`(A:Set)`, for example:
-
-   .. coqtop:: all
-
-      Check list_ind.
-
-   Once again, the types of the constructor arguments and of the conclusion can be omitted:
-
-   .. coqtop:: none
-
-      Reset list.
-
-   .. coqtop:: in
-
-      Inductive list (A:Set) : Set := nil | cons (_:A) (_:list A).
-
-.. note::
-   + The constructor type can
-     recursively invoke the inductive definition on an argument which is not
-     the parameter itself.
-
-     One can define :
-
-     .. coqtop:: all
-
-        Inductive list2 (A:Set) : Set :=
-        | nil2 : list2 A
-        | cons2 : A -> list2 (A*A) -> list2 A.
-
-     that can also be written by specifying only the type of the arguments:
-
-     .. coqtop:: all reset
-
-        Inductive list2 (A:Set) : Set :=
-        | nil2
-        | cons2 (_:A) (_:list2 (A*A)).
-
-     But the following definition will give an error:
-
-     .. coqtop:: all
-
-        Fail Inductive listw (A:Set) : Set :=
-        | nilw : listw (A*A)
-        | consw : A -> listw (A*A) -> listw (A*A).
-
-     because the conclusion of the type of constructors should be :g:`listw A`
-     in both cases.
-
-   + A parameterized inductive definition can be defined using annotations
-     instead of parameters but it will sometimes give a different (bigger)
-     sort for the inductive definition and will produce a less convenient
-     rule for case elimination.
-
-.. flag:: Uniform Inductive Parameters
-
-     When this flag is set (it is off by default),
-     inductive definitions are abstracted over their parameters
-     before type checking constructors, allowing to write:
-
-     .. coqtop:: all
-
-        Set Uniform Inductive Parameters.
-        Inductive list3 (A:Set) : Set :=
-        | nil3 : list3
-        | cons3 : A -> list3 -> list3.
-
-     This behavior is essentially equivalent to starting a new section
-     and using :cmd:`Context` to give the uniform parameters, like so
-     (cf. :ref:`section-mechanism`):
-
-     .. coqtop:: all reset
-
-        Section list3.
-        Context (A:Set).
-        Inductive list3 : Set :=
-        | nil3 : list3
-        | cons3 : A -> list3 -> list3.
-        End list3.
-
-     For finer control, you can use a ``|`` between the uniform and
-     the non-uniform parameters:
-
-     .. coqtop:: in reset
-
-        Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop
-          := Acc_in : (forall y, R y x -> Acc y) -> Acc x.
-
-     The flag can then be seen as deciding whether the ``|`` is at the
-     beginning (when the flag is unset) or at the end (when it is set)
-     of the parameters when not explicitly given.
-
-.. seealso::
-   Section :ref:`inductive-definitions` and the :tacn:`induction` tactic.
-
-.. _mutually_inductive_types:
-
-Mutually defined inductive types
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-.. example:: Mutually defined inductive types
-
-   A typical example of mutually inductive data types is trees and
-   forests. We assume two types :g:`A` and :g:`B` that are given as variables. The types can
-   be declared like this:
-
-   .. coqtop:: in
-
-      Parameters A B : Set.
-
-      Inductive tree : Set := node : A -> forest -> tree
-
-      with forest : Set :=
-      | leaf : B -> forest
-      | cons : tree -> forest -> forest.
-
-   This declaration automatically generates eight induction principles. They are not the most
-   general principles, but they correspond to each inductive part seen as a single inductive definition.
-
-   To illustrate this point on our example, here are the types of :g:`tree_rec`
-   and :g:`forest_rec`.
-
-   .. coqtop:: all
-
-      Check tree_rec.
-
-      Check forest_rec.
-
-   Assume we want to parameterize our mutual inductive definitions with the
-   two type variables :g:`A` and :g:`B`, the declaration should be
-   done as follows:
-
-   .. coqdoc::
-
-      Inductive tree (A B:Set) : Set := node : A -> forest A B -> tree A B
-
-      with forest (A B:Set) : Set :=
-      | leaf : B -> forest A B
-      | cons : tree A B -> forest A B -> forest A B.
-
-   Assume we define an inductive definition inside a section
-   (cf. :ref:`section-mechanism`). When the section is closed, the variables
-   declared in the section and occurring free in the declaration are added as
-   parameters to the inductive definition.
-
-.. seealso::
-   A generic command :cmd:`Scheme` is useful to build automatically various
-   mutual induction principles.
-
-Private (matching) inductive types
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-.. attr:: private(matching)
-
-   This attribute can be used to forbid the use of the :g:`match`
-   construct on objects of this inductive type outside of the module
-   where it is defined.  There is also a legacy syntax using the
-   ``Private`` prefix (cf. :n:`@legacy_attr`).
-
-   The main use case of private (matching) inductive types is to emulate
-   quotient types / higher-order inductive types in projects such as
-   the `HoTT library <https://github.com/HoTT/HoTT>`_.
-
-.. example::
-
-   .. coqtop:: all
-
-      Module Foo.
-      #[ private(matching) ] Inductive my_nat := my_O : my_nat | my_S : my_nat -> my_nat.
-      Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).
-      End Foo.
-      Import Foo.
-      Fail Check (fun x : my_nat => match x with my_O => true | my_S _ => false end).
-
-Variants
-~~~~~~~~
-
-.. cmd:: Variant @variant_definition {* with @variant_definition }
-
-   .. insertprodn variant_definition variant_definition
-
-   .. prodn::
-      variant_definition ::= @ident_decl {* @binder } {? %| {* @binder } } {? : @type } := {? %| } {+| @constructor } {? @decl_notations }
-
-   The :cmd:`Variant` command is similar to the :cmd:`Inductive` command, except
-   that it disallows recursive definition of types (for instance, lists cannot
-   be defined using :cmd:`Variant`). No induction scheme is generated for
-   this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on.
-
-   This command supports the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`universes(template)`,
-   :attr:`universes(notemplate)`, :attr:`universes(cumulative)`,
-   :attr:`universes(noncumulative)` and :attr:`private(matching)`
-   attributes.
-
-   .. exn:: The @num th argument of @ident must be @ident in @type.
-      :undocumented:
-
-.. _coinductive-types:
-
-Co-inductive types
-------------------
-
-The objects of an inductive type are well-founded with respect to the
-constructors of the type. In other words, such objects contain only a
-*finite* number of constructors. Co-inductive types arise from relaxing
-this condition, and admitting types whose objects contain an infinity of
-constructors. Infinite objects are introduced by a non-ending (but
-effective) process of construction, defined in terms of the constructors
-of the type.
-
-.. cmd:: CoInductive @inductive_definition {* with @inductive_definition }
-
-   This command introduces a co-inductive type.
-   The syntax of the command is the same as the command :cmd:`Inductive`.
-   No principle of induction is derived from the definition of a co-inductive
-   type, since such principles only make sense for inductive types.
-   For co-inductive types, the only elimination principle is case analysis.
-
-   This command supports the :attr:`universes(polymorphic)`,
-   :attr:`universes(monomorphic)`, :attr:`universes(template)`,
-   :attr:`universes(notemplate)`, :attr:`universes(cumulative)`,
-   :attr:`universes(noncumulative)` and :attr:`private(matching)`
-   attributes.
-
-.. example::
-
-   The type of infinite sequences of natural numbers, usually called streams,
-   is an example of a co-inductive type.
-
-   .. coqtop:: in
-
-      CoInductive Stream : Set := Seq : nat -> Stream -> Stream.
-
-   The usual destructors on streams :g:`hd:Stream->nat` and :g:`tl:Str->Str`
-   can be defined as follows:
-
-   .. coqtop:: in
-
-      Definition hd (x:Stream) := let (a,s) := x in a.
-      Definition tl (x:Stream) := let (a,s) := x in s.
-
-Definitions of co-inductive predicates and blocks of mutually
-co-inductive definitions are also allowed.
-
-.. example::
-
-   The extensional equality on streams is an example of a co-inductive type:
-
-   .. coqtop:: in
-
-      CoInductive EqSt : Stream -> Stream -> Prop :=
-        eqst : forall s1 s2:Stream,
-                 hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
-
-   In order to prove the extensional equality of two streams :g:`s1` and :g:`s2`
-   we have to construct an infinite proof of equality, that is, an infinite
-   object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite
-   objects in Section :ref:`cofixpoint`.
-
-Caveat
-~~~~~~
-
-The ability to define co-inductive types by constructors, hereafter called
-*positive co-inductive types*, is known to break subject reduction. The story is
-a bit long: this is due to dependent pattern-matching which implies
-propositional η-equality, which itself would require full η-conversion for
-subject reduction to hold, but full η-conversion is not acceptable as it would
-make type checking undecidable.
-
-Since the introduction of primitive records in Coq 8.5, an alternative
-presentation is available, called *negative co-inductive types*. This consists
-in defining a co-inductive type as a primitive record type through its
-projections. Such a technique is akin to the *co-pattern* style that can be
-found in e.g. Agda, and preserves subject reduction.
-
-The above example can be rewritten in the following way.
-
-.. coqtop:: none
-
-   Reset Stream.
-
-.. coqtop:: all
-
-   Set Primitive Projections.
-   CoInductive Stream : Set := Seq { hd : nat; tl : Stream }.
-   CoInductive EqSt (s1 s2: Stream) : Prop := eqst {
-     eqst_hd : hd s1 = hd s2;
-     eqst_tl : EqSt (tl s1) (tl s2);
-   }.
-
-Some properties that hold over positive streams are lost when going to the
-negative presentation, typically when they imply equality over streams.
-For instance, propositional η-equality is lost when going to the negative
-presentation. It is nonetheless logically consistent to recover it through an
-axiom.
-
-.. coqtop:: all
-
-   Axiom Stream_eta : forall s: Stream, s = Seq (hd s) (tl s).
-
-More generally, as in the case of positive coinductive types, it is consistent
-to further identify extensional equality of coinductive types with propositional
-equality:
-
-.. coqtop:: all
-
-   Axiom Stream_ext : forall (s1 s2: Stream), EqSt s1 s2 -> s1 = s2.
-
-As of Coq 8.9, it is now advised to use negative co-inductive types rather than
-their positive counterparts.
-
-.. seealso::
-   :ref:`primitive_projections` for more information about negative
-   records and primitive projections.
-
-
-Definition of recursive functions
----------------------------------
-
-Definition of functions by recursion over inductive objects
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-This section describes the primitive form of definition by recursion over
-inductive objects. See the :cmd:`Function` command for more advanced
-constructions.
-
-.. _Fixpoint:
-
-.. cmd:: Fixpoint @fix_definition {* with @fix_definition }
-
-   .. insertprodn fix_definition fix_definition
-
-   .. prodn::
-      fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @type } {? := @term } {? @decl_notations }
-
-   This command 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
-   corresponding to these :n:`@binder`\s has type :n:`@type`, and is
-   equivalent to the expression :n:`@term`. The type of :n:`@ident` is
-   consequently :n:`forall {* @binder }, @type` and its value is equivalent
-   to :n:`fun {* @binder } => @term`.
-
-   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.
-   The point of the :n:`{struct @ident}` annotation (see :n:`@fixannot`) is to
-   let the user tell the system which argument decreases along the recursive calls.
-
-   The :n:`{struct @ident}` annotation may be left implicit, in which case the
-   system successively tries arguments from left to right until it finds one
-   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`.
-
-   The :n:`with` clause allows simultaneously defining several mutual fixpoints.
-   It is especially useful when defining functions over mutually defined
-   inductive types.  Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`.
-
-   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
-   This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
-   In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
-   for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
-
-   .. note::
-
-      + Some fixpoints may have several arguments that fit as decreasing
-        arguments, and this choice influences the reduction of the fixpoint.
-        Hence an explicit annotation must be used if the leftmost decreasing
-        argument is not the desired one. Writing explicit annotations can also
-        speed up type checking of large mutual fixpoints.
-
-      + In order to keep the strong normalization property, the fixed point
-        reduction will only be performed when the argument in position of the
-        decreasing argument (which type should be in an inductive definition)
-        starts with a constructor.
-
-
-   .. example::
-
-      One can define the addition function as :
-
-      .. coqtop:: all
-
-         Fixpoint add (n m:nat) {struct n} : nat :=
-         match n with
-         | O => m
-         | S p => S (add p m)
-         end.
-
-      The match operator matches a value (here :g:`n`) with the various
-      constructors of its (inductive) type. The remaining arguments give the
-      respective values to be returned, as functions of the parameters of the
-      corresponding constructor. Thus here when :g:`n` equals :g:`O` we return
-      :g:`m`, and when :g:`n` equals :g:`(S p)` we return :g:`(S (add p m))`.
-
-      The match operator is formally described in
-      Section :ref:`match-construction`.
-      The system recognizes that in the inductive call :g:`(add p m)` the first
-      argument actually decreases because it is a *pattern variable* coming
-      from :g:`match n with`.
-
-   .. example::
-
-      The following definition is not correct and generates an error message:
-
-      .. coqtop:: all
-
-         Fail Fixpoint wrongplus (n m:nat) {struct n} : nat :=
-         match m with
-         | O => n
-         | S p => S (wrongplus n p)
-         end.
-
-      because the declared decreasing argument :g:`n` does not actually
-      decrease in the recursive call. The function computing the addition over
-      the second argument should rather be written:
-
-      .. coqtop:: all
-
-         Fixpoint plus (n m:nat) {struct m} : nat :=
-         match m with
-         | O => n
-         | S p => S (plus n p)
-         end.
-
-   .. example::
-
-      The recursive call may not only be on direct subterms of the recursive
-      variable :g:`n` but also on a deeper subterm and we can directly write
-      the function :g:`mod2` which gives the remainder modulo 2 of a natural
-      number.
-
-      .. coqtop:: all
-
-         Fixpoint mod2 (n:nat) : nat :=
-         match n with
-         | O => O
-         | S p => match p with
-                  | O => S O
-                  | S q => mod2 q
-                  end
-         end.
-
-.. _example_mutual_fixpoints:
-
-   .. example:: Mutual fixpoints
-
-      The size of trees and forests can be defined the following way:
-
-      .. coqtop:: all
-
-         Fixpoint tree_size (t:tree) : nat :=
-         match t with
-         | node a f => S (forest_size f)
-         end
-         with forest_size (f:forest) : nat :=
-         match f with
-         | leaf b => 1
-         | cons t f' => (tree_size t + forest_size f')
-         end.
-
-.. _cofixpoint:
-
-Definitions of recursive objects in co-inductive types
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-.. cmd:: CoFixpoint @cofix_definition {* with @cofix_definition }
-
-   .. insertprodn cofix_definition cofix_definition
-
-   .. prodn::
-      cofix_definition ::= @ident_decl {* @binder } {? : @type } {? := @term } {? @decl_notations }
-
-   This command introduces a method for constructing an infinite object of a
-   coinductive type. For example, the stream containing all natural numbers can
-   be introduced applying the following method to the number :g:`O` (see
-   Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd`
-   and :g:`tl`):
-
-   .. coqtop:: all
-
-      CoFixpoint from (n:nat) : Stream := Seq n (from (S n)).
-
-   Unlike recursive definitions, there is no decreasing argument in a
-   co-recursive definition. To be admissible, a method of construction must
-   provide at least one extra constructor of the infinite object for each
-   iteration. A syntactical guard condition is imposed on co-recursive
-   definitions in order to ensure this: each recursive call in the
-   definition must be protected by at least one constructor, and only by
-   constructors. That is the case in the former definition, where the single
-   recursive call of :g:`from` is guarded by an application of :g:`Seq`.
-   On the contrary, the following recursive function does not satisfy the
-   guard condition:
-
-   .. coqtop:: all
-
-      Fail CoFixpoint filter (p:nat -> bool) (s:Stream) : Stream :=
-        if p (hd s) then Seq (hd s) (filter p (tl s)) else filter p (tl s).
-
-   The elimination of co-recursive definition is done lazily, i.e. the
-   definition is expanded only when it occurs at the head of an application
-   which is the argument of a case analysis expression. In any other
-   context, it is considered as a canonical expression which is completely
-   evaluated. We can test this using the command :cmd:`Eval`, which computes
-   the normal forms of a term:
-
-   .. coqtop:: all
-
-      Eval compute in (from 0).
-      Eval compute in (hd (from 0)).
-      Eval compute in (tl (from 0)).
-
-   As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously
-   defining several mutual cofixpoints.
-
-   If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
-   This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
-   In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
-   for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
-
-.. _Computations:
-
-Computations
-------------
-
-.. insertprodn reduce pattern_occ
-
-.. prodn::
-   reduce ::= Eval @red_expr in
-   red_expr ::= red
-   | hnf
-   | simpl {? @delta_flag } {? @ref_or_pattern_occ }
-   | cbv {? @strategy_flag }
-   | cbn {? @strategy_flag }
-   | lazy {? @strategy_flag }
-   | compute {? @delta_flag }
-   | vm_compute {? @ref_or_pattern_occ }
-   | native_compute {? @ref_or_pattern_occ }
-   | unfold {+, @unfold_occ }
-   | fold {+ @one_term }
-   | pattern {+, @pattern_occ }
-   | @ident
-   delta_flag ::= {? - } [ {+ @smart_qualid } ]
-   strategy_flag ::= {+ @red_flags }
-   | @delta_flag
-   red_flags ::= beta
-   | iota
-   | match
-   | fix
-   | cofix
-   | zeta
-   | delta {? @delta_flag }
-   ref_or_pattern_occ ::= @smart_qualid {? at @occs_nums }
-   | @one_term {? at @occs_nums }
-   occs_nums ::= {+ {| @num | @ident } }
-   | - {| @num | @ident } {* @int_or_var }
-   int_or_var ::= @int
-   | @ident
-   unfold_occ ::= @smart_qualid {? at @occs_nums }
-   pattern_occ ::= @one_term {? at @occs_nums }
-
-See :ref:`Conversion-rules`.
-
-.. todo:: Add text here
-
-.. _Assertions:
-
-Assertions and proofs
----------------------
-
-An assertion states a proposition (or a type) of which the proof (or an
-inhabitant of the type) is interactively built using tactics. The interactive
-proof mode is described in Chapter :ref:`proofhandling` and the tactics in
-Chapter :ref:`Tactics`. The basic assertion command is:
-
-.. cmd:: @thm_token @ident_decl {* @binder } : @type {* with @ident_decl {* @binder } : @type }
-   :name: Theorem; Lemma; Fact; Remark; Corollary; Proposition; Property
-
-   .. insertprodn thm_token thm_token
-
-   .. prodn::
-      thm_token ::= Theorem
-      | Lemma
-      | Fact
-      | Remark
-      | Corollary
-      | Proposition
-      | Property
-
-   After the statement is asserted, Coq needs a proof. Once a proof of
-   :n:`@type` under the assumptions represented by :n:`@binder`\s is given and
-   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.
-
-   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
-   :cmd:`Fixpoint` or :cmd:`CoFixpoint` but using tactics to build the proof of
-   the statements (or the body of the specification, depending on the point of
-   view). The inductive or co-inductive types on which the induction or
-   coinduction has to be done is assumed to be non ambiguous and is guessed by
-   the system.
-
-   Like in a :cmd:`Fixpoint` or :cmd:`CoFixpoint` definition, the induction hypotheses
-   have to be used on *structurally smaller* arguments (for a :cmd:`Fixpoint`) or
-   be *guarded by a constructor* (for a :cmd:`CoFixpoint`). The verification that
-   recursive proof arguments are correct is done only at the time of registering
-   the lemma in the environment. To know if the use of induction hypotheses is
-   correct at some time of the interactive development of a proof, use the
-   command :cmd:`Guarded`.
-
-   .. exn:: The term @term has type @type which should be Set, Prop or Type.
-      :undocumented:
-
-   .. exn:: @ident already exists.
-      :name: @ident already exists. (Theorem)
-
-      The name you provided is already defined. You have then to choose
-      another name.
-
-   .. exn:: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on.
-
-      You are asserting a new statement while already being in proof editing mode.
-      This feature, called nested proofs, is disabled by default.
-      To activate it, turn the :flag:`Nested Proofs Allowed` flag on.
-
-Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode
-until the proof is completed. In proof editing mode, the user primarily enters
-tactics, which are described in chapter :ref:`Tactics`. The user may also enter
-commands to manage the proof editing mode. They are described in Chapter
-:ref:`proofhandling`.
-
-When the proof is complete, use the :cmd:`Qed` command so the kernel verifies
-the proof and adds it to the environment.
-
-.. note::
-
-   #. Several statements can be simultaneously asserted provided the
-      :flag:`Nested Proofs Allowed` flag was turned on.
-
-   #. Not only other assertions but any vernacular command can be given
-      while in the process of proving a given assertion. In this case, the
-      command is understood as if it would have been given before the
-      statements still to be proved. Nonetheless, this practice is discouraged
-      and may stop working in future versions.
-
-   #. Proofs ended by :cmd:`Qed` are declared opaque. Their content cannot be
-      unfolded (see :ref:`performingcomputations`), thus
-      realizing some form of *proof-irrelevance*. To be able to unfold a
-      proof, the proof should be ended by :cmd:`Defined`.
-
-   #. :cmd:`Proof` is recommended but can currently be omitted. On the opposite
-      side, :cmd:`Qed` (or :cmd:`Defined`) is mandatory to validate a proof.
-
-   #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the
-      current asserted statement into an axiom and exit the proof editing mode.
-
-.. [1]
-   Except if the inductive type is empty in which case there is no
-   equation that can be used to infer the return type.