Extract section on implicit arguments from Gallina extensions.

1 files changed, 0 insertions, 1693 deletions

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 18b05e47d3..fb762a00f1 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1,1374 +1,3 @@
-.. _extensionsofgallina:
-
-Extensions of |Gallina|
-=======================
-
-|Gallina| is the kernel language of |Coq|. We describe here extensions of
-|Gallina|’s syntax.
-
-.. _record-types:
-
-Record types
-----------------
-
-The :cmd:`Record` construction is a macro allowing the definition of
-records as is done in many programming languages. Its syntax is
-described in the grammar below. In fact, the :cmd:`Record` macro is more general
-than the usual record types, since it allows also for “manifest”
-expressions. In this sense, the :cmd:`Record` construction allows defining
-“signatures”.
-
-.. _record_grammar:
-
-.. cmd:: {| Record | Structure } @record_definition {* with @record_definition }
-   :name: Record; Structure
-
-   .. insertprodn record_definition field_body
-
-   .. prodn::
-      record_definition ::= {? > } @ident_decl {* @binder } {? : @type } {? @ident } %{ {*; @record_field } %} {? @decl_notations }
-      record_field ::= {* #[ {*, @attr } ] } @name {? @field_body } {? %| @num } {? @decl_notations }
-      field_body ::= {* @binder } @of_type
-      | {* @binder } @of_type := @term
-      | {* @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`.
-   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.
-
-   Notations can be attached to fields using the :n:`@decl_notations` annotation.
-
-   :cmd:`Record` and :cmd:`Structure` are synonyms.
-
-   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.
-
-More generally, a record may have explicitly defined (a.k.a. manifest)
-fields. For instance, we might have:
-:n:`Record @ident {* @binder } : @sort := { @ident__1 : @type__1 ; @ident__2 := @term__2 ; @ident__3 : @type__3 }`.
-in which case the correctness of :n:`@type__3` may rely on the instance :n:`@term__2` of :n:`@ident__2` and :n:`@term__2` may in turn depend on :n:`@ident__1`.
-
-.. example::
-
-   The set of rational numbers may be defined as:
-
-   .. coqtop:: reset all
-
-      Record Rat : Set := mkRat
-       { sign : bool
-       ; top : nat
-       ; bottom : nat
-       ; Rat_bottom_cond : 0 <> bottom
-       ; Rat_irred_cond :
-           forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1
-       }.
-
-   Note here that the fields ``Rat_bottom_cond`` depends on the field ``bottom``
-   and ``Rat_irred_cond`` depends on both ``top`` and ``bottom``.
-
-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
-:n:`@ident__0` with the appropriate number of terms filling the fields of the record.
-
-.. example::
-
-   Let us define the rational :math:`1/2`:
-
-    .. coqtop:: in
-
-       Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1.
-       Admitted.
-
-       Definition half := mkRat true 1 2 (O_S 1) one_two_irred.
-       Check half.
-
-Alternatively, the following syntax allows creating objects by using named fields, as
-shown in this grammar. The fields do not have to be in any particular order, nor do they have
-to be all present if the missing ones can be inferred or prompted for
-(see :ref:`programs`).
-
-.. coqtop:: all
-
-  Definition half' :=
-    {| sign := true;
-       Rat_bottom_cond := O_S 1;
-       Rat_irred_cond := one_two_irred |}.
-
-The following settings let you control the display format for types:
-
-.. flag:: Printing Records
-
-   If set, use the record syntax (shown above) as the default display format.
-
-You can override the display format for specified types by adding entries to these tables:
-
-.. table:: Printing Record @qualid
-   :name: Printing Record
-
-   Specifies a set of qualids which are displayed as records.  Use the
-   :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids.
-
-.. table:: Printing Constructor @qualid
-   :name: Printing Constructor
-
-   Specifies a set of qualids which are displayed as constructors.  Use the
-   :cmd:`Add @table` and :cmd:`Remove @table` commands to update the set of qualids.
-
-This syntax can also be used for pattern matching.
-
-.. coqtop:: all
-
-   Eval compute in (
-     match half with
-     | {| sign := true; top := n |} => n
-     | _ => 0
-     end).
-
-The macro generates also, when it is possible, the projection
-functions for destructuring an object of type :token:`ident`. These
-projection functions are given the names of the corresponding
-fields. If a field is named `_` then no projection is built
-for it. In our example:
-
-.. coqtop:: all
-
-  Eval compute in top half.
-  Eval compute in bottom half.
-  Eval compute in Rat_bottom_cond half.
-
-An alternative syntax for projections based on a dot notation is
-available:
-
-.. coqtop:: all
-
-   Eval compute in half.(top).
-
-.. flag:: Printing Projections
-
-   This flag activates the dot notation for printing.
-
-   .. example::
-
-      .. coqtop:: all
-
-         Set Printing Projections.
-         Check top half.
-
-.. FIXME: move this to the main grammar in the spec chapter
-
-.. _record_projections_grammar:
-
-  .. insertprodn term_projection term_projection
-
-  .. prodn::
-     term_projection ::= @term0 .( @qualid {* @arg } )
-     | @term0 .( @ @qualid {* @term1 } )
-
-  Syntax of Record projections
-
-The corresponding grammar rules are given in the preceding grammar. When :token:`qualid`
-denotes a projection, the syntax :n:`@term0.(@qualid)` is equivalent to :n:`@qualid @term0`,
-the syntax :n:`@term0.(@qualid {+ @arg })` to :n:`@qualid {+ @arg } @term0`.
-and the syntax :n:`@term0.(@@qualid {+ @term0 })` to :n:`@@qualid {+ @term0 } @term0`.
-In each case, :token:`term0` is the object projected and the
-other arguments are the parameters of the inductive type.
-
-
-.. note:: Records defined with the ``Record`` keyword are not allowed to be
-   recursive (references to the record's name in the type of its field
-   raises an  error). To define recursive records, one can use the ``Inductive``
-   and ``CoInductive`` keywords, resulting in an inductive or co-inductive record.
-   Definition of mutually inductive or co-inductive records are also allowed, as long
-   as all of the types in the block are records.
-
-.. note:: Induction schemes are automatically generated for inductive records.
-   Automatic generation of induction schemes for non-recursive records
-   defined with the ``Record`` keyword can be activated with the
-   :flag:`Nonrecursive Elimination Schemes` flag (see :ref:`proofschemes-induction-principles`).
-
-.. warn:: @ident cannot be defined.
-
-  It can happen that the definition of a projection is impossible.
-  This message is followed by an explanation of this impossibility.
-  There may be three reasons:
-
-  #. The name :token:`ident` already exists in the environment (see :cmd:`Axiom`).
-  #. The body of :token:`ident` uses an incorrect elimination for
-     :token:`ident` (see :cmd:`Fixpoint` and :ref:`Destructors`).
-  #. The type of the projections :token:`ident` depends on previous
-     projections which themselves could not be defined.
-
-.. exn:: Records declared with the keyword Record or Structure cannot be recursive.
-
-   The record name :token:`ident` appears in the type of its fields, but uses
-   the keyword ``Record``. Use  the keyword ``Inductive`` or ``CoInductive`` instead.
-
-.. exn:: Cannot handle mutually (co)inductive records.
-
-   Records cannot be defined as part of mutually inductive (or
-   co-inductive) definitions, whether with records only or mixed with
-   standard definitions.
-
-During the definition of the one-constructor inductive definition, all
-the errors of inductive definitions, as described in Section
-:ref:`gallina-inductive-definitions`, may also occur.
-
-.. seealso:: Coercions and records in section :ref:`coercions-classes-as-records` of the chapter devoted to coercions.
-
-.. _primitive_projections:
-
-Primitive Projections
-~~~~~~~~~~~~~~~~~~~~~
-
-.. flag:: Primitive Projections
-
-   Turns on the use of primitive
-   projections when defining subsequent records (even through the ``Inductive``
-   and ``CoInductive`` commands). Primitive projections
-   extended the Calculus of Inductive Constructions with a new binary
-   term constructor `r.(p)` representing a primitive projection `p` applied
-   to a record object `r` (i.e., primitive projections are always applied).
-   Even if the record type has parameters, these do not appear
-   in the internal representation of
-   applications of the projection, considerably reducing the sizes of
-   terms when manipulating parameterized records and type checking time.
-   On the user level, primitive projections can be used as a replacement
-   for the usual defined ones, although there are a few notable differences.
-
-.. flag:: Printing Primitive Projection Parameters
-
-   This compatibility flag reconstructs internally omitted parameters at
-   printing time (even though they are absent in the actual AST manipulated
-   by the kernel).
-
-Primitive Record Types
-++++++++++++++++++++++
-
-When the :flag:`Primitive Projections` flag is on, definitions of
-record types change meaning. When a type is declared with primitive
-projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though).
-To eliminate the (co-)inductive type, one must use its defined primitive projections.
-
-.. The following paragraph is quite redundant with what is above
-
-For compatibility, the parameters still appear to the user when
-printing terms even though they are absent in the actual AST
-manipulated by the kernel. This can be changed by unsetting the
-:flag:`Printing Primitive Projection Parameters` flag.
-
-There are currently two ways to introduce primitive records types:
-
-#. Through the ``Record`` command, in which case the type has to be
-   non-recursive. The defined type enjoys eta-conversion definitionally,
-   that is the generalized form of surjective pairing for records:
-   `r` ``= Build_``\ `R` ``(``\ `r`\ ``.(``\ |p_1|\ ``) …`` `r`\ ``.(``\ |p_n|\ ``))``.
-   Eta-conversion allows to define dependent elimination for these types as well.
-#. Through the ``Inductive`` and ``CoInductive`` commands, when
-   the body of the definition is a record declaration of the form
-   ``Build_``\ `R` ``{`` |p_1| ``:`` |t_1|\ ``; … ;`` |p_n| ``:`` |t_n| ``}``.
-   In this case the types can be recursive and eta-conversion is disallowed. These kind of record types
-   differ from their traditional versions in the sense that dependent
-   elimination is not available for them and only non-dependent case analysis
-   can be defined.
-
-Reduction
-+++++++++
-
-The basic reduction rule of a primitive projection is
-|p_i| ``(Build_``\ `R` |t_1| … |t_n|\ ``)`` :math:`{\rightarrow_{\iota}}` |t_i|.
-However, to take the :math:`{\delta}` flag into
-account, projections can be in two states: folded or unfolded. An
-unfolded primitive projection application obeys the rule above, while
-the folded version delta-reduces to the unfolded version. This allows to
-precisely mimic the usual unfolding rules of constants. Projections
-obey the usual ``simpl`` flags of the ``Arguments`` command in particular.
-There is currently no way to input unfolded primitive projections at the
-user-level, and there is no way to display unfolded projections differently
-from folded ones.
-
-
-Compatibility Projections and :g:`match`
-++++++++++++++++++++++++++++++++++++++++
-
-To ease compatibility with ordinary record types, each primitive
-projection is also defined as a ordinary constant taking parameters and
-an object of the record type as arguments, and whose body is an
-application of the unfolded primitive projection of the same name. These
-constants are used when elaborating partial applications of the
-projection. One can distinguish them from applications of the primitive
-projection if the :flag:`Printing Primitive Projection Parameters` flag
-is off: For a primitive projection application, parameters are printed
-as underscores while for the compatibility projections they are printed
-as usual.
-
-Additionally, user-written :g:`match` constructs on primitive records
-are desugared into substitution of the projections, they cannot be
-printed back as :g:`match` constructs.
-
-Variants and extensions of :g:`match`
--------------------------------------
-
-.. _mult-match:
-
-Multiple and nested pattern matching
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The basic version of :g:`match` allows pattern matching on simple
-patterns. As an extension, multiple nested patterns or disjunction of
-patterns are allowed, as in ML-like languages.
-
-The extension just acts as a macro that is expanded during parsing
-into a sequence of match on simple patterns. Especially, a
-construction defined using the extended match is generally printed
-under its expanded form (see :flag:`Printing Matching`).
-
-.. seealso:: :ref:`extendedpatternmatching`.
-
-.. _if-then-else:
-
-Pattern-matching on boolean values: the if expression
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-For inductive types with exactly two constructors and for pattern matching
-expressions that do not depend on the arguments of the constructors, it is possible
-to use a ``if … then … else`` notation. For instance, the definition
-
-.. coqtop:: all
-
-   Definition not (b:bool) :=
-   match b with
-   | true => false
-   | false => true
-   end.
-
-can be alternatively written
-
-.. coqtop:: reset all
-
-   Definition not (b:bool) := if b then false else true.
-
-More generally, for an inductive type with constructors :n:`@ident__1`
-and :n:`@ident__2`, the following terms are equal:
-
-:n:`if @term__0 {? {? as @name } return @term } then @term__1 else @term__2`
-
-:n:`match @term__0 {? {? as @name } return @term } with | @ident__1 {* _ } => @term__1 | @ident__2 {* _ } => @term__2 end`
-
-.. example::
-
-  .. coqtop:: all
-
-     Check (fun x (H:{x=0}+{x<>0}) =>
-     match H with
-     | left _ => true
-     | right _ => false
-     end).
-
-Notice that the printing uses the :g:`if` syntax because :g:`sumbool` is
-declared as such (see :ref:`controlling-match-pp`).
-
-.. _irrefutable-patterns:
-
-Irrefutable patterns: the destructuring let variants
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Pattern-matching on terms inhabiting inductive type having only one
-constructor can be alternatively written using :g:`let … in …`
-constructions. There are two variants of them.
-
-
-First destructuring let syntax
-++++++++++++++++++++++++++++++
-
-The expression :n:`let ( {*, @ident__i } ) := @term__0 in @term__1`
-performs case analysis on :n:`@term__0` whose type must be an
-inductive type with exactly one constructor.  The number of variables
-:n:`@ident__i` must correspond to the number of arguments of this
-contrustor.  Then, in :n:`@term__1`, these variables are bound to the
-arguments of the constructor in :n:`@term__0`.  For instance, the
-definition
-
-.. coqtop:: reset all
-
-   Definition fst (A B:Set) (H:A * B) := match H with
-   | pair x y => x
-   end.
-
-can be alternatively written
-
-.. coqtop:: reset all
-
-   Definition fst (A B:Set) (p:A * B) := let (x, _) := p in x.
-
-Notice that reduction is different from regular :g:`let … in …`
-construction since it happens only if :n:`@term__0` is in constructor form.
-Otherwise, the reduction is blocked.
-
-The pretty-printing of a definition by matching on a irrefutable
-pattern can either be done using :g:`match` or the :g:`let` construction
-(see Section :ref:`controlling-match-pp`).
-
-If term inhabits an inductive type with one constructor `C`, we have an
-equivalence between
-
-::
-
-   let (ident₁, …, identₙ) [dep_ret_type] := term in term'
-
-and
-
-::
-
-   match term [dep_ret_type] with
-   C ident₁ … identₙ => term'
-   end
-
-
-Second destructuring let syntax
-+++++++++++++++++++++++++++++++
-
-Another destructuring let syntax is available for inductive types with
-one constructor by giving an arbitrary pattern instead of just a tuple
-for all the arguments. For example, the preceding example can be
-written:
-
-.. coqtop:: reset all
-
-   Definition fst (A B:Set) (p:A*B) := let 'pair x _ := p in x.
-
-This is useful to match deeper inside tuples and also to use notations
-for the pattern, as the syntax :g:`let ’p := t in b` allows arbitrary
-patterns to do the deconstruction. For example:
-
-.. coqtop:: all
-
-   Definition deep_tuple (A:Set) (x:(A*A)*(A*A)) : A*A*A*A :=
-   let '((a,b), (c, d)) := x in (a,b,c,d).
-
-   Notation " x 'With' p " := (exist _ x p) (at level 20).
-
-   Definition proj1_sig' (A:Set) (P:A->Prop) (t:{ x:A | P x }) : A :=
-   let 'x With p := t in x.
-
-When printing definitions which are written using this construct it
-takes precedence over let printing directives for the datatype under
-consideration (see Section :ref:`controlling-match-pp`).
-
-
-.. _controlling-match-pp:
-
-Controlling pretty-printing of match expressions
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The following commands give some control over the pretty-printing
-of :g:`match` expressions.
-
-Printing nested patterns
-+++++++++++++++++++++++++
-
-.. flag:: Printing Matching
-
-   The Calculus of Inductive Constructions knows pattern matching only
-   over simple patterns. It is however convenient to re-factorize nested
-   pattern matching into a single pattern matching over a nested
-   pattern.
-
-   When this flag is on (default), |Coq|’s printer tries to do such
-   limited re-factorization.
-   Turning it off tells |Coq| to print only simple pattern matching problems
-   in the same way as the |Coq| kernel handles them.
-
-
-Factorization of clauses with same right-hand side
-++++++++++++++++++++++++++++++++++++++++++++++++++
-
-.. flag:: Printing Factorizable Match Patterns
-
-   When several patterns share the same right-hand side, it is additionally
-   possible to share the clauses using disjunctive patterns. Assuming that the
-   printing matching mode is on, this flag (on by default) tells |Coq|'s
-   printer to try to do this kind of factorization.
-
-Use of a default clause
-+++++++++++++++++++++++
-
-.. flag:: Printing Allow Match Default Clause
-
-   When several patterns share the same right-hand side which do not depend on the
-   arguments of the patterns, yet an extra factorization is possible: the
-   disjunction of patterns can be replaced with a `_` default clause. Assuming that
-   the printing matching mode and the factorization mode are on, this flag (on by
-   default) tells |Coq|'s printer to use a default clause when relevant.
-
-Printing of wildcard patterns
-++++++++++++++++++++++++++++++
-
-.. flag:: Printing Wildcard
-
-   Some variables in a pattern may not occur in the right-hand side of
-   the pattern matching clause. When this flag is on (default), the
-   variables having no occurrences in the right-hand side of the
-   pattern matching clause are just printed using the wildcard symbol
-   “_”.
-
-
-Printing of the elimination predicate
-+++++++++++++++++++++++++++++++++++++
-
-.. flag:: Printing Synth
-
-   In most of the cases, the type of the result of a matched term is
-   mechanically synthesizable. Especially, if the result type does not
-   depend of the matched term. When this flag is on (default),
-   the result type is not printed when |Coq| knows that it can re-
-   synthesize it.
-
-
-Printing matching on irrefutable patterns
-++++++++++++++++++++++++++++++++++++++++++
-
-If an inductive type has just one constructor, pattern matching can be
-written using the first destructuring let syntax.
-
-.. table:: Printing Let @qualid
-   :name: Printing Let
-
-   Specifies a set of qualids for which pattern matching is displayed using a let expression.
-   Note that this only applies to pattern matching instances entered with :g:`match`.
-   It doesn't affect pattern matching explicitly entered with a destructuring
-   :g:`let`.
-   Use the :cmd:`Add @table` and :cmd:`Remove @table` commands to update this set.
-
-
-Printing matching on booleans
-+++++++++++++++++++++++++++++
-
-If an inductive type is isomorphic to the boolean type, pattern matching
-can be written using ``if`` … ``then`` … ``else`` ….  This table controls
-which types are written this way:
-
-.. table:: Printing If @qualid
-   :name: Printing If
-
-   Specifies a set of qualids for which pattern matching is displayed using
-   ``if`` … ``then`` … ``else`` ….  Use the :cmd:`Add @table` and :cmd:`Remove @table`
-   commands to update this set.
-
-This example emphasizes what the printing settings offer.
-
-.. example::
-
-     .. coqtop:: all
-
-       Definition snd (A B:Set) (H:A * B) := match H with
-       | pair x y => y
-       end.
-
-       Test Printing Let for prod.
-
-       Print snd.
-
-       Remove Printing Let prod.
-
-       Unset Printing Synth.
-
-       Unset Printing Wildcard.
-
-       Print snd.
-
-.. _advanced-recursive-functions:
-       
-Advanced recursive functions
-----------------------------
-
-The following command is available when the ``FunInd`` library has been loaded via ``Require Import FunInd``:
-
-.. cmd:: Function @fix_definition {* with @fix_definition }
-
-   This command is a generalization of :cmd:`Fixpoint`. It is a wrapper
-   for several ways of defining a function *and* other useful related
-   objects, namely: an induction principle that reflects the recursive
-   structure of the function (see :tacn:`function induction`) and its fixpoint equality.
-   This defines a function similar to those defined by :cmd:`Fixpoint`.
-   As in :cmd:`Fixpoint`, the decreasing argument must
-   be given (unless the function is not recursive), but it might not
-   necessarily be *structurally* decreasing. Use the :n:`@fixannot` clause
-   to name the decreasing argument *and* to describe which kind of
-   decreasing criteria to use to ensure termination of recursive
-   calls.
-
-   :cmd:`Function` also supports the :n:`with` clause to create
-   mutually recursive definitions, however this feature is limited
-   to structurally recursive functions (i.e. when :n:`@fixannot` is a :n:`struct`
-   clause).
-
-   See :tacn:`function induction` and :cmd:`Functional Scheme` for how to use
-   the induction principle to reason easily about the function.
-
-   The form of the :n:`@fixannot` clause determines which definition mechanism :cmd:`Function` uses.
-   (Note that references to :n:`ident` below refer to the name of the function being defined.):
-
-   *  If :n:`@fixannot` is not specified, :cmd:`Function`
-      defines the nonrecursive function :token:`ident` as if it was declared with
-      :cmd:`Definition`. In addition, the following are defined:
-
-       + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``,
-         which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`);
-       + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently);
-       + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which
-         are inversion information linking the function and its graph.
-
-   *  If :n:`{ struct ... }` is specified, :cmd:`Function`
-      defines the structural recursive function :token:`ident` as if it was declared
-      with :cmd:`Fixpoint`. In addition, the following are defined:
-
-       + The same objects as above;
-       + The fixpoint equation of :token:`ident`: :n:`@ident`\ ``_equation``.
-
-   *  If :n:`{ measure ... }` or :n:`{ wf ... }` are specified, :cmd:`Function`
-      defines a recursive function by well-founded recursion. The module ``Recdef``
-      of the standard library must be loaded for this feature.
-
-       + :n:`{measure @one_term__1 {? @ident } {? @one_term__2 } }`\: where :n:`@ident` is the decreasing argument
-         and :n:`@one_term__1` is a function from the type of :n:`@ident` to :g:`nat` for which
-         the decreasing argument decreases (for the :g:`lt` order on :g:`nat`)
-         for each recursive call of the function. The parameters of the function are
-         bound in :n:`@one_term__1`.
-       + :n:`{wf @one_term @ident }`\: where :n:`@ident` is the decreasing argument and
-         :n:`@one_term` is an ordering relation on the type of :n:`@ident` (i.e. of type
-         `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument
-         decreases for each recursive call of the function. The order must be well-founded.
-         The parameters of the function are bound in :n:`@one_term`.
-
-      If the clause is ``measure`` or ``wf``, the user is left with some proof
-      obligations that will be used to define the function. These proofs
-      are: proofs that each recursive call is actually decreasing with
-      respect to the given criteria, and (if the criteria is `wf`) a proof
-      that the ordering relation is well-founded. Once proof obligations are
-      discharged, the following objects are defined:
-
-        + The same objects as with the ``struct`` clause;
-        + The lemma :n:`@ident`\ ``_tcc`` which collects all proof obligations in one
-          property;
-        + The lemmas :n:`@ident`\ ``_terminate`` and :n:`@ident`\ ``_F`` which will be inlined
-          during extraction of :n:`@ident`.
-
-      The way this recursive function is defined is the subject of several
-      papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles
-      Barthe, Julien Forest, David Pichardie, and Vlad Rusu on the other
-      hand.
-
-.. note::
-
-   To obtain the right principle, it is better to put rigid
-   parameters of the function as first arguments. For example it is
-   better to define plus like this:
-
-   .. coqtop:: reset none
-
-      Require Import FunInd.
-
-   .. coqtop:: all
-
-      Function plus (m n : nat) {struct n} : nat :=
-      match n with
-      | 0 => m
-      | S p => S (plus m p)
-      end.
-
-   than like this:
-
-   .. coqtop:: reset none
-
-      Require Import FunInd.
-
-   .. coqtop:: all
-
-      Function plus (n m : nat) {struct n} : nat :=
-      match n with
-      | 0 => m
-      | S p => S (plus p m)
-      end.
-
-
-*Limitations*
-
-:token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`)
-with applications only *at the end* of each branch.
-
-:cmd:`Function` does not support partial application of the function being
-defined. Thus, the following example cannot be accepted due to the
-presence of partial application of :g:`wrong` in the body of :g:`wrong`:
-
-.. coqtop:: none
-
-   Require List.
-   Import List.ListNotations.
-
-.. coqtop:: all fail
-
-   Function wrong (C:nat) : nat :=
-     List.hd 0 (List.map wrong (C::nil)).
-
-For now, dependent cases are not treated for non structurally
-terminating functions.
-
-.. exn:: The recursive argument must be specified.
-   :undocumented:
-
-.. exn:: No argument name @ident.
-   :undocumented:
-
-.. exn:: Cannot use mutual definition with well-founded recursion or measure.
-   :undocumented:
-
-.. warn:: Cannot define graph for @ident.
-
-   The generation of the graph relation (:n:`R_@ident`) used to compute the induction scheme of ident
-   raised a typing error. Only :token:`ident` is defined; the induction scheme
-   will not be generated. This error happens generally when:
-
-   - the definition uses pattern matching on dependent types,
-     which :cmd:`Function` cannot deal with yet.
-   - the definition is not a *pattern matching tree* as explained above.
-
-.. warn:: Cannot define principle(s) for @ident.
-
-   The generation of the graph relation (:n:`R_@ident`) succeeded but the induction principle
-   could not be built. Only :token:`ident` is defined. Please report.
-
-.. warn:: Cannot build functional inversion principle.
-
-   :tacn:`functional inversion` will not be available for the function.
-
-.. seealso:: :ref:`functional-scheme` and :tacn:`function induction`
-
-.. _section-mechanism:
-
-Section mechanism
------------------
-
-Sections create local contexts which can be shared across multiple definitions.
-
-.. example::
-
-   Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`.
-
-   .. coqtop:: all
-
-      Section s1.
-
-   Inside a section, local parameters can be introduced using :cmd:`Variable`,
-   :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for
-   the first two).
-
-   .. coqtop:: all
-
-      Variables x y : nat.
-
-   The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions
-   won't persist when the section is closed, and all persistent definitions which
-   depend on `y'` will be prefixed with `let y' := y in`.
-
-   .. coqtop:: in
-
-      Let y' := y.
-      Definition x' := S x.
-      Definition x'' := x' + y'.
-
-   .. coqtop:: all
-
-      Print x'.
-      Print x''.
-
-      End s1.
-
-      Print x'.
-      Print x''.
-
-   Notice the difference between the value of :g:`x'` and :g:`x''` inside section
-   :g:`s1` and outside.
-
-.. cmd:: Section @ident
-
-   This command is used to open a section named :token:`ident`.
-   Section names do not need to be unique.
-
-
-.. cmd:: End @ident
-
-   This command closes the section or module named :token:`ident`.
-   See :ref:`Terminating an interactive module or module type definition<terminating_module>`
-   for a description of its use with modules.
-
-   After closing the
-   section, the local declarations (variables and local definitions, see :cmd:`Variable`) are
-   *discharged*, meaning that they stop being visible and that all global
-   objects defined in the section are generalized with respect to the
-   variables and local definitions they each depended on in the section.
-
-   .. exn:: There is nothing to end.
-      :undocumented:
-
-   .. exn:: Last block to end has name @ident.
-       :undocumented:
-
-.. note::
-   Most commands, like :cmd:`Hint`, :cmd:`Notation`, option management, … which
-   appear inside a section are canceled when the section is closed.
-
-.. cmd:: Let @ident @def_body
-         Let Fixpoint @fix_definition {* with @fix_definition }
-         Let CoFixpoint @cofix_definition {* with @cofix_definition }
-   :name: Let; Let Fixpoint; Let CoFixpoint
-
-   These commands behave like :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that
-   the declared constant is local to the current section.
-   When the section is closed, all persistent
-   definitions and theorems within it that depend on the constant
-   will be wrapped with a :n:`@term_let` with the same declaration.
-
-   As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`,
-   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`.
-
-.. cmd:: Context {+ @binder }
-
-   Declare variables in the context of the current section, like :cmd:`Variable`,
-   but also allowing implicit variables, :ref:`implicit-generalization`, and
-   let-binders.
-
-   .. coqdoc::
-
-     Context {A : Type} (a b : A).
-     Context `{EqDec A}.
-     Context (b' := b).
-
-.. seealso:: Section :ref:`binders`. Section :ref:`contexts` in chapter :ref:`typeclasses`.
-
-Module system
--------------
-
-The module system provides a way of packaging related elements
-together, as well as a means of massive abstraction.
-
-
-.. cmd:: Module {? {| Import | Export } } @ident {* @module_binder } {? @of_module_type } {? := {+<+ @module_expr_inl } }
-
-   .. insertprodn module_binder module_expr_inl
-
-   .. prodn::
-      module_binder ::= ( {? {| Import | Export } } {+ @ident } : @module_type_inl )
-      module_type_inl ::= ! @module_type
-      | @module_type {? @functor_app_annot }
-      functor_app_annot ::= [ inline at level @num ]
-      | [ no inline ]
-      module_type ::= @qualid
-      | ( @module_type )
-      | @module_type @module_expr_atom
-      | @module_type with @with_declaration
-      with_declaration ::= Definition @qualid {? @univ_decl } := @term
-      | Module @qualid := @qualid
-      module_expr_atom ::= @qualid
-      | ( {+ @module_expr_atom } )
-      of_module_type ::= : @module_type_inl
-      | {* <: @module_type_inl }
-      module_expr_inl ::= ! {+ @module_expr_atom }
-      | {+ @module_expr_atom } {? @functor_app_annot }
-
-   Defines a module named :token:`ident`.  See the examples :ref:`here<module_examples>`.
-
-   The :n:`Import` and :n:`Export` flags specify whether the module should be automatically
-   imported or exported.
-
-   Specifying :n:`{* @module_binder }` starts a functor with
-   parameters given by the :n:`@module_binder`\s.  (A *functor* is a function
-   from modules to modules.)
-
-   .. todo: would like to find a better term than "interactive", not very descriptive
-
-   :n:`@of_module_type` specifies the module type.  :n:`{+ <: @module_type_inl }`
-   starts a module that satisfies each :n:`@module_type_inl`.
-
-   :n:`:= {+<+ @module_expr_inl }` specifies the body of a module or functor
-   definition.  If it's not specified, then the module is defined *interactively*,
-   meaning that the module is defined as a series of commands terminated with :cmd:`End`
-   instead of in a single :cmd:`Module` command.
-   Interactively defining the :n:`@module_expr_inl`\s in a series of
-   :cmd:`Include` commands is equivalent to giving them all in a single
-   non-interactive :cmd:`Module` command.
-
-   The ! prefix indicates that any assumption command (such as :cmd:`Axiom`) with an :n:`Inline` clause
-   in the type of the functor arguments will be ignored.
-
-   .. todo: What is an Inline directive?  sb command but still unclear.  Maybe referring to the
-      "inline" in functor_app_annot?  or assumption_token Inline assum_list?
-
-.. cmd:: Module Type @ident {* @module_binder } {* <: @module_type_inl } {? := {+<+ @module_type_inl } }
-
-   Defines a module type named :n:`@ident`.  See the example :ref:`here<example_def_simple_module_type>`.
-
-   Specifying :n:`{* @module_binder }` starts a functor type with
-   parameters given by the :n:`@module_binder`\s.
-
-   :n:`:= {+<+ @module_type_inl }` specifies the body of a module or functor type
-   definition.  If it's not specified, then the module type is defined *interactively*,
-   meaning that the module type is defined as a series of commands terminated with :cmd:`End`
-   instead of in a single :cmd:`Module Type` command.
-   Interactively defining the :n:`@module_type_inl`\s in a series of
-   :cmd:`Include` commands is equivalent to giving them all in a single
-   non-interactive :cmd:`Module Type` command.
-
-.. _terminating_module:
-
-**Terminating an interactive module or module type definition**
-
-Interactive modules are terminated with the :cmd:`End` command, which
-is also used to terminate :ref:`Sections<section-mechanism>`.
-:n:`End @ident` closes the interactive module or module type :token:`ident`.
-If the module type was given, the command verifies that the content of the module
-matches the module type.  If the module is not a
-functor, its components (constants, inductive types, submodules etc.)
-are now available through the dot notation.
-
-.. exn:: No such label @ident.
-    :undocumented:
-
-.. exn:: Signature components for label @ident do not match.
-    :undocumented:
-
-.. exn:: The field @ident is missing in @qualid.
-   :undocumented:
-
-.. |br| raw:: html
-
-    <br>
-
-.. note::
-
-  #. 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
-     modules and module types. Note that with module definitions like:
-
-     :n:`Module @ident__1 : @module_type := @ident__2.`
-
-     or
-
-     :n:`Module @ident__1 : @module_type.` |br|
-     :n:`Include @ident__2.` |br|
-     :n:`End @ident__1.`
-
-     hints and the like valid for :n:`@ident__1` are the ones defined in :n:`@module_type`
-     rather then those defined in :n:`@ident__2` (or the module body).
-  #. Within an interactive module type definition, the :cmd:`Parameter` command declares a
-     constant instead of definining a new axiom (which it does when not in a module type definition).
-  #. Assumptions such as :cmd:`Axiom` that include the :n:`Inline` clause will be automatically
-     expanded when the functor is applied, except when the function application is prefixed by ``!``.
-
-.. cmd:: Include @module_type_inl {* <+ @module_expr_inl }
-
-   Includes the content of module(s) in the current
-   interactive module. Here :n:`@module_type_inl` can be a module expression or a module
-   type expression. If it is a high-order module or module type
-   expression then the system tries to instantiate :n:`@module_type_inl` with the current
-   interactive module.
-
-   Including multiple modules is a single :cmd:`Include` is equivalent to including each module
-   in a separate :cmd:`Include` command.
-
-.. cmd:: Include Type {+<+ @module_type_inl }
-
-   .. deprecated:: 8.3
-
-      Use :cmd:`Include` instead.
-
-.. cmd:: Declare Module {? {| Import | Export } } @ident {* @module_binder } : @module_type_inl
-
-   Declares a module :token:`ident` of type :token:`module_type_inl`.
-
-   If :n:`@module_binder`\s are specified, declares a functor with parameters given by the list of
-   :token:`module_binder`\s.
-
-.. cmd:: Import {+ @qualid }
-
-   If :token:`qualid` denotes a valid basic module (i.e. its module type is a
-   signature), makes its components available by their short names.
-
-   .. example::
-
-      .. coqtop:: reset in
-
-         Module Mod.
-         Definition T:=nat.
-         Check T.
-         End Mod.
-         Check Mod.T.
-
-      .. coqtop:: all
-
-         Fail Check T.
-         Import Mod.
-         Check T.
-
-   Some features defined in modules are activated only when a module is
-   imported. This is for instance the case of notations (see :ref:`Notations`).
-
-   Declarations made with the :attr:`local` attribute are never imported by the :cmd:`Import`
-   command. Such declarations are only accessible through their fully
-   qualified name.
-
-   .. example::
-
-      .. coqtop:: in
-
-         Module A.
-         Module B.
-         Local Definition T := nat.
-         End B.
-         End A.
-         Import A.
-
-      .. coqtop:: all fail
-
-         Check B.T.
-
-.. cmd:: Export {+ @qualid }
-   :name: Export
-
-   Similar to :cmd:`Import`, except that when the module containing this command
-   is imported, the :n:`{+ @qualid }` are imported as well.
-
-   .. exn:: @qualid is not a module.
-      :undocumented:
-
-   .. warn:: Trying to mask the absolute name @qualid!
-      :undocumented:
-
-.. cmd:: Print Module @qualid
-
-   Prints the module type and (optionally) the body of the module :n:`@qualid`.
-
-.. cmd:: Print Module Type @qualid
-
-   Prints the module type corresponding to :n:`@qualid`.
-
-.. flag:: Short Module Printing
-
-   This flag (off by default) disables the printing of the types of fields,
-   leaving only their names, for the commands :cmd:`Print Module` and
-   :cmd:`Print Module Type`.
-
-.. _module_examples:
-
-Examples
-~~~~~~~~
-
-.. example:: Defining a simple module interactively
-
-    .. coqtop:: in
-
-       Module M.
-       Definition T := nat.
-       Definition x := 0.
-
-    .. coqtop:: all
-
-       Definition y : bool.
-       exact true.
-
-    .. coqtop:: in
-
-       Defined.
-       End M.
-
-Inside a module one can define constants, prove theorems and do anything
-else that can be done in the toplevel. Components of a closed
-module can be accessed using the dot notation:
-
-.. coqtop:: all
-
-   Print M.x.
-
-.. _example_def_simple_module_type:
-
-.. example:: Defining a simple module type interactively
-
-   .. coqtop:: in
-
-      Module Type SIG.
-      Parameter T : Set.
-      Parameter x : T.
-      End SIG.
-
-.. _example_filter_module:
-
-.. example:: Creating a new module that omits some items from an existing module
-
-   Since :n:`SIG`, the type of the new module :n:`N`, doesn't define :n:`y` or
-   give the body of :n:`x`, which are not included in :n:`N`.
-
-   .. coqtop:: all
-
-      Module N : SIG with Definition T := nat := M.
-      Print N.T.
-      Print N.x.
-      Fail Print N.y.
-
-   .. reset to remove N (undo in last coqtop block doesn't seem to do that), invisibly redefine M, SIG
-   .. coqtop:: none reset
-
-      Module M.
-      Definition T := nat.
-      Definition x := 0.
-      Definition y : bool.
-      exact true.
-      Defined.
-      End M.
-
-      Module Type SIG.
-      Parameter T : Set.
-      Parameter x : T.
-      End SIG.
-
-The following definition of :g:`N` using the module type expression :g:`SIG` with
-:g:`Definition T := nat` is equivalent to the following one:
-
-.. todo: what is other definition referred to above?
-   "Module N' : SIG with Definition T := nat. End N`." is not it.
-
-.. coqtop:: in
-
-   Module Type SIG'.
-   Definition T : Set := nat.
-   Parameter x : T.
-   End SIG'.
-
-   Module N : SIG' := M.
-
-If we just want to be sure that our implementation satisfies a
-given module type without restricting the interface, we can use a
-transparent constraint
-
-.. coqtop:: in
-
-   Module P <: SIG := M.
-
-.. coqtop:: all
-
-   Print P.y.
-
-.. example:: Creating a functor (a module with parameters)
-
-   .. coqtop:: in
-
-      Module Two (X Y: SIG).
-      Definition T := (X.T * Y.T)%type.
-      Definition x := (X.x, Y.x).
-      End Two.
-
-   and apply it to our modules and do some computations:
-
-   .. coqtop:: in
-
-
-      Module Q := Two M N.
-
-   .. coqtop:: all
-
-      Eval compute in (fst Q.x + snd Q.x).
-
-.. example:: A module type with two sub-modules, sharing some fields
-
-   .. coqtop:: in
-
-      Module Type SIG2.
-        Declare Module M1 : SIG.
-        Module M2 <: SIG.
-          Definition T := M1.T.
-          Parameter x : T.
-        End M2.
-      End SIG2.
-
-   .. coqtop:: in
-
-      Module Mod <: SIG2.
-        Module M1.
-          Definition T := nat.
-          Definition x := 1.
-        End M1.
-      Module M2 := M.
-      End Mod.
-
-Notice that ``M`` is a correct body for the component ``M2`` since its ``T``
-component is ``nat`` as specified for ``M1.T``.
-
-Libraries and qualified names
----------------------------------
-
-.. _names-of-libraries:
-
-Names of libraries
-~~~~~~~~~~~~~~~~~~
-
-The theories developed in |Coq| are stored in *library files* which are
-hierarchically classified into *libraries* and *sublibraries*. To
-express this hierarchy, library names are represented by qualified
-identifiers qualid, i.e. as list of identifiers separated by dots (see
-:ref:`gallina-identifiers`). For instance, the library file ``Mult`` of the standard
-|Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts
-the name of a library is called a *library root*. All library files of
-the standard library of |Coq| have the reserved root |Coq| but library
-filenames based on other roots can be obtained by using |Coq| commands
-(coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`command-line-options`).
-Also, when an interactive |Coq| session starts, a library of root ``Top`` is
-started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-options`).
-
-.. _qualified-names:
-
-Qualified names
-~~~~~~~~~~~~~~~
-
-Library files are modules which possibly contain submodules which
-eventually contain constructions (axioms, parameters, definitions,
-lemmas, theorems, remarks or facts). The *absolute name*, or *full
-name*, of a construction in some library file is a qualified
-identifier starting with the logical name of the library file,
-followed by the sequence of submodules names encapsulating the
-construction and ended by the proper name of the construction.
-Typically, the absolute name ``Coq.Init.Logic.eq`` denotes Leibniz’
-equality defined in the module Logic in the sublibrary ``Init`` of the
-standard library of |Coq|.
-
-The proper name that ends the name of a construction is the short name
-(or sometimes base name) of the construction (for instance, the short
-name of ``Coq.Init.Logic.eq`` is ``eq``). Any partial suffix of the absolute
-name is a *partially qualified name* (e.g. ``Logic.eq`` is a partially
-qualified name for ``Coq.Init.Logic.eq``). Especially, the short name of a
-construction is its shortest partially qualified name.
-
-|Coq| does not accept two constructions (definition, theorem, …) with
-the same absolute name but different constructions can have the same
-short name (or even same partially qualified names as soon as the full
-names are different).
-
-Notice that the notion of absolute, partially qualified and short
-names also applies to library filenames.
-
-**Visibility**
-
-|Coq| maintains a table called the name table which maps partially qualified
-names of constructions to absolute names. This table is updated by the
-commands :cmd:`Require`, :cmd:`Import` and :cmd:`Export` and
-also each time a new declaration is added to the context. An absolute
-name is called visible from a given short or partially qualified name
-when this latter name is enough to denote it. This means that the
-short or partially qualified name is mapped to the absolute name in
-|Coq| name table. Definitions with the :attr:`local` attribute are only accessible with
-their fully qualified name (see :ref:`gallina-definitions`).
-
-It may happen that a visible name is hidden by the short name or a
-qualified name of another construction. In this case, the name that
-has been hidden must be referred to using one more level of
-qualification. To ensure that a construction always remains
-accessible, absolute names can never be hidden.
-
-.. example::
-
-    .. coqtop:: all
-
-       Check 0.
-
-       Definition nat := bool.
-
-       Check 0.
-
-       Check Datatypes.nat.
-
-       Locate nat.
-
-.. seealso:: Commands :cmd:`Locate` and :cmd:`Locate Library`.
-
-.. _libraries-and-filesystem:
-
-Libraries and filesystem
-~~~~~~~~~~~~~~~~~~~~~~~~
-
-.. note:: The questions described here have been subject to redesign in |Coq| 8.5.
-   Former versions of |Coq| use the same terminology to describe slightly different things.
-
-Compiled files (``.vo`` and ``.vio``) store sub-libraries. In order to refer
-to them inside |Coq|, a translation from file-system names to |Coq| names
-is needed. In this translation, names in the file system are called
-*physical* paths while |Coq| names are contrastingly called *logical*
-names.
-
-A logical prefix Lib can be associated with a physical path using
-the command line option ``-Q`` `path` ``Lib``. All subfolders of path are
-recursively associated to the logical path ``Lib`` extended with the
-corresponding suffix coming from the physical path. For instance, the
-folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding
-to invalid |Coq| identifiers are skipped, and, by convention,
-subdirectories named ``CVS`` or ``_darcs`` are skipped too.
-
-Thanks to this mechanism, ``.vo`` files are made available through the
-logical name of the folder they are in, extended with their own
-basename. For example, the name associated to the file
-``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for
-invalid identifiers. When compiling a source file, the ``.vo`` file stores
-its logical name, so that an error is issued if it is loaded with the
-wrong loadpath afterwards.
-
-Some folders have a special status and are automatically put in the
-path. |Coq| commands associate automatically a logical path to files in
-the repository trees rooted at the directory from where the command is
-launched, ``coqlib/user-contrib/``, the directories listed in the
-``$COQPATH``, ``${XDG_DATA_HOME}/coq/`` and ``${XDG_DATA_DIRS}/coq/``
-environment variables (see `XDG base directory specification
-<http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html>`_)
-with the same physical-to-logical translation and with an empty logical prefix.
-
-The command line option ``-R`` is a variant of ``-Q`` which has the strictly
-same behavior regarding loadpaths, but which also makes the
-corresponding ``.vo`` files available through their short names in a way
-similar to the :cmd:`Import` command. For instance, ``-R path Lib``
-associates to the file ``/path/fOO/Bar/File.vo`` the logical name
-``Lib.fOO.Bar.File``, but allows this file to be accessed through the
-short names ``fOO.Bar.File,Bar.File`` and ``File``. If several files with
-identical base name are present in different subdirectories of a
-recursive loadpath, which of these files is found first may be system-
-dependent and explicit qualification is recommended. The ``From`` argument
-of the ``Require`` command can be used to bypass the implicit shortening
-by providing an absolute root to the required file (see :ref:`compiled-files`).
-
-There also exists another independent loadpath mechanism attached to
-OCaml object files (``.cmo`` or ``.cmxs``) rather than |Coq| object
-files as described above. The OCaml loadpath is managed using
-the option ``-I`` `path` (in the OCaml world, there is neither a
-notion of logical name prefix nor a way to access files in
-subdirectories of path). See the command :cmd:`Declare ML Module` in
-:ref:`compiled-files` to understand the need of the OCaml loadpath.
-
-See :ref:`command-line-options` for a more general view over the |Coq| command
-line options.
-
 .. _ImplicitArguments:
 
 Implicit arguments
@@ -2272,325 +901,3 @@ Multiple binders can be merged using ``,`` as a separator:
 
    The :n:`No Variables` form disables implicit generalization entirely.  This is
    the default behavior (before any :cmd:`Generalizable` command has been entered).
-
-
-.. _Coercions:
-
-Coercions
----------
-
-Coercions can be used to implicitly inject terms from one *class* in
-which they reside into another one. A *class* is either a sort
-(denoted by the keyword ``Sortclass``), a product type (denoted by the
-keyword ``Funclass``), or a type constructor (denoted by its name), e.g.
-an inductive type or any constant with a type of the form
-:n:`forall {+ @binder }, @sort`.
-
-Then the user is able to apply an object that is not a function, but
-can be coerced to a function, and more generally to consider that a
-term of type ``A`` is of type ``B`` provided that there is a declared coercion
-between ``A`` and ``B``.
-
-More details and examples, and a description of the commands related
-to coercions are provided in :ref:`implicitcoercions`.
-
-.. _printing_constructions_full:
-
-Printing constructions in full
-------------------------------
-
-.. flag:: Printing All
-
-   Coercions, implicit arguments, the type of pattern matching, but also
-   notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some
-   tactics (typically the tactics applying to occurrences of subterms are
-   sensitive to the implicit arguments). Turning this flag on
-   deactivates all high-level printing features such as coercions,
-   implicit arguments, returned type of pattern matching, notations and
-   various syntactic sugar for pattern matching or record projections.
-   Otherwise said, :flag:`Printing All` includes the effects of the flags
-   :flag:`Printing Implicit`, :flag:`Printing Coercions`, :flag:`Printing Synth`,
-   :flag:`Printing Projections`, and :flag:`Printing Notations`. To reactivate
-   the high-level printing features, use the command ``Unset Printing All``.
-
-.. _printing-universes:
-
-Printing universes
-------------------
-
-.. flag:: Printing Universes
-
-   Turn this flag on to activate the display of the actual level of each
-   occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard flag, in
-   combination with :flag:`Printing All` can help to diagnose failures to unify
-   terms apparently identical but internally different in the Calculus of Inductive
-   Constructions.
-
-.. cmd:: Print {? Sorted } Universes {? Subgraph ( {* @qualid } ) } {? @string }
-   :name: Print Universes
-
-   This command can be used to print the constraints on the internal level
-   of the occurrences of :math:`\Type` (see :ref:`Sorts`).
-
-   The :n:`Subgraph` clause limits the printed graph to the requested names (adjusting
-   constraints to preserve the implied transitive constraints between
-   kept universes).
-
-   The :n:`Sorted` clause makes each universe
-   equivalent to a numbered label reflecting its level (with a linear
-   ordering) in the universe hierarchy.
-
-   :n:`@string` is an optional output filename.
-   If :n:`@string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT
-   language, and can be processed by Graphviz tools. The format is
-   unspecified if `string` doesn’t end in ``.dot`` or ``.gv``.
-
-.. _existential-variables:
-
-Existential variables
----------------------
-
-.. insertprodn term_evar term_evar
-
-.. prodn::
-   term_evar ::= ?[ @ident ]
-   | ?[ ?@ident ]
-   | ?@ident {? @%{ {+; @ident := @term } %} }
-
-|Coq| terms can include existential variables which represents unknown
-subterms to eventually be replaced by actual subterms.
-
-Existential variables are generated in place of unsolvable implicit
-arguments or “_” placeholders when using commands such as ``Check`` (see
-Section :ref:`requests-to-the-environment`) or when using tactics such as
-:tacn:`refine`, as well as in place of unsolvable instances when using
-tactics such that :tacn:`eapply`. An existential
-variable is defined in a context, which is the context of variables of
-the placeholder which generated the existential variable, and a type,
-which is the expected type of the placeholder.
-
-As a consequence of typing constraints, existential variables can be
-duplicated in such a way that they possibly appear in different
-contexts than their defining context. Thus, any occurrence of a given
-existential variable comes with an instance of its original context.
-In the simple case, when an existential variable denotes the
-placeholder which generated it, or is used in the same context as the
-one in which it was generated, the context is not displayed and the
-existential variable is represented by “?” followed by an identifier.
-
-.. coqtop:: all
-
-   Parameter identity : forall (X:Set), X -> X.
-
-   Check identity _ _.
-
-   Check identity _ (fun x => _).
-
-In the general case, when an existential variable :n:`?@ident` appears
-outside of its context of definition, its instance, written under the
-form :n:`{ {*; @ident := @term} }` is appending to its name, indicating
-how the variables of its defining context are instantiated.
-The variables of the context of the existential variables which are
-instantiated by themselves are not written, unless the :flag:`Printing Existential Instances` flag
-is on (see Section :ref:`explicit-display-existentials`), and this is why an
-existential variable used in the same context as its context of definition is written with no instance.
-
-.. coqtop:: all
-
-   Check (fun x y => _) 0 1.
-
-   Set Printing Existential Instances.
-
-   Check (fun x y => _) 0 1.
-
-Existential variables can be named by the user upon creation using
-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`).
-
-.. _explicit-display-existentials:
-
-Explicit displaying of existential instances for pretty-printing
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-.. flag:: Printing Existential Instances
-
-   This flag (off by default) activates the full display of how the
-   context of an existential variable is instantiated at each of the
-   occurrences of the existential variable.
-
-.. _tactics-in-terms:
-
-Solving existential variables using tactics
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-Instead of letting the unification engine try to solve an existential
-variable by itself, one can also provide an explicit hole together
-with a tactic to solve it. Using the syntax ``ltac:(``\ `tacexpr`\ ``)``, the user
-can put a tactic anywhere a term is expected. The order of resolution
-is not specified and is implementation-dependent. The inner tactic may
-use any variable defined in its scope, including repeated alternations
-between variables introduced by term binding as well as those
-introduced by tactic binding. The expression `tacexpr` can be any tactic
-expression as described in :ref:`ltac`.
-
-.. coqtop:: all
-
-   Definition foo (x : nat) : nat := ltac:(exact x).
-
-This construction is useful when one wants to define complicated terms
-using highly automated tactics without resorting to writing the proof-term
-by means of the interactive proof engine.
-
-.. _primitive-integers:
-
-Primitive Integers
-------------------
-
-The language of terms features 63-bit machine integers as values. The type of
-such a value is *axiomatized*; it is declared through the following sentence
-(excerpt from the :g:`Int63` module):
-
-.. coqdoc::
-
-   Primitive int := #int63_type.
-
-This type is equipped with a few operators, that must be similarly declared.
-For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function,
-declared and specified as follows:
-
-.. coqdoc::
-
-   Primitive eqb := #int63_eq.
-   Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope.
-
-   Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j.
-
-The complete set of such operators can be obtained looking at the :g:`Int63` module.
-
-These primitive declarations are regular axioms. As such, they must be trusted and are listed by the
-:g:`Print Assumptions` command, as in the following example.
-
-.. coqtop:: in reset
-
-   From Coq Require Import Int63.
-   Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63.
-   Proof. apply eqb_correct; vm_compute; reflexivity. Qed.
-
-.. coqtop:: all
-
-   Print Assumptions one_minus_one_is_zero.
-
-The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement
-dedicated, efficient, rules to reduce the applications of these primitive
-operations.
-
-The extraction of these primitives can be customized similarly to the extraction
-of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlInt63`
-module can be used when extracting to OCaml: it maps the Coq primitives to types
-and functions of a :g:`Uint63` module. Said OCaml module is not produced by
-extraction. Instead, it has to be provided by the user (if they want to compile
-or execute the extracted code). For instance, an implementation of this module
-can be taken from the kernel of Coq.
-
-Literal values (at type :g:`Int63.int`) are extracted to literal OCaml values
-wrapped into the :g:`Uint63.of_int` (resp. :g:`Uint63.of_int64`) constructor on
-64-bit (resp. 32-bit) platforms. Currently, this cannot be customized (see the
-function :g:`Uint63.compile` from the kernel).
-
-.. _primitive-floats:
-
-Primitive Floats
-----------------
-
-The language of terms features Binary64 floating-point numbers as values.
-The type of such a value is *axiomatized*; it is declared through the
-following sentence (excerpt from the :g:`PrimFloat` module):
-
-.. coqdoc::
-
-   Primitive float := #float64_type.
-
-This type is equipped with a few operators, that must be similarly declared.
-For instance, the product of two primitive floats can be computed using the
-:g:`PrimFloat.mul` function, declared and specified as follows:
-
-.. coqdoc::
-
-   Primitive mul := #float64_mul.
-   Notation "x * y" := (mul x y) : float_scope.
-
-   Axiom mul_spec : forall x y, Prim2SF (x * y)%float = SF64mul (Prim2SF x) (Prim2SF y).
-
-where :g:`Prim2SF` is defined in the :g:`FloatOps` module.
-
-The set of such operators is described in section :ref:`floats_library`.
-
-These primitive declarations are regular axioms. As such, they must be trusted, and are listed by the
-:g:`Print Assumptions` command.
-
-The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement
-dedicated, efficient rules to reduce the applications of these primitive
-operations, using the floating-point processor operators that are assumed
-to comply with the IEEE 754 standard for floating-point arithmetic.
-
-The extraction of these primitives can be customized similarly to the extraction
-of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlFloats`
-module can be used when extracting to OCaml: it maps the Coq primitives to types
-and functions of a :g:`Float64` module. Said OCaml module is not produced by
-extraction. Instead, it has to be provided by the user (if they want to compile
-or execute the extracted code). For instance, an implementation of this module
-can be taken from the kernel of Coq.
-
-Literal values (of type :g:`Float64.t`) are extracted to literal OCaml
-values (of type :g:`float`) written in hexadecimal notation and
-wrapped into the :g:`Float64.of_float` constructor, e.g.:
-:g:`Float64.of_float (0x1p+0)`.
-
-.. _bidirectionality_hints:
-
-Bidirectionality hints
-----------------------
-
-When type-checking an application, Coq normally does not use information from
-the context to infer the types of the arguments. It only checks after the fact
-that the type inferred for the application is coherent with the expected type.
-Bidirectionality hints make it possible to specify that after type-checking the
-first arguments of an application, typing information should be propagated from
-the context to help inferring the types of the remaining arguments.
-
-An :cmd:`Arguments` command containing :n:`@argument_spec_block__1 & @argument_spec_block__2`
-provides :ref:`bidirectionality_hints`.
-It tells the typechecking algorithm, when type-checking
-applications of :n:`@qualid`, to first type-check the arguments in
-:n:`@argument_spec_block__1` and then propagate information from the typing context to
-type-check the remaining arguments (in :n:`@argument_spec_block__2`).
-
-.. example:: Bidirectionality hints
-
-   In a context where a coercion was declared from ``bool`` to ``nat``:
-
-   .. coqtop:: in reset
-
-      Definition b2n (b : bool) := if b then 1 else 0.
-      Coercion b2n : bool >-> nat.
-
-   Coq cannot automatically coerce existential statements over ``bool`` to
-   statements over ``nat``, because the need for inserting a coercion is known
-   only from the expected type of a subterm:
-
-   .. coqtop:: all
-
-      Fail Check (ex_intro _ true _ : exists n : nat, n > 0).
-
-   However, a suitable bidirectionality hint makes the example work:
-
-   .. coqtop:: all
-
-      Arguments ex_intro _ _ & _ _.
-      Check (ex_intro _ true _ : exists n : nat, n > 0).
-
-Coq will attempt to produce a term which uses the arguments you
-provided, but in some cases involving Program mode the arguments after
-the bidirectionality starts may be replaced by convertible but
-syntactically different terms.