11 files changed, 142 insertions, 47 deletions
diff --git a/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst
new file mode 100644
index 0000000000..bac08d12ea
--- /dev/null
+++ b/doc/changelog/01-kernel/10664-sections-stack-in-kernel.rst
@@ -0,0 +1,6 @@
+- Section data is now part of the kernel. Solves a soundness issue
+  in interactive mode where global monomorphic universe constraints would be
+  dropped when forcing a delayed opaque proof inside a polymorphic section. Also
+  relaxes the nesting criterion for sections, as polymorphic sections can now
+  appear inside a monomorphic one
+  (#10664, <https://github.com/coq/coq/pull/10664> by Pierre-Marie Pédrot).
diff --git a/doc/changelog/02-specification-language/10758-fix-10757.rst b/doc/changelog/02-specification-language/10758-fix-10757.rst
new file mode 100644
index 0000000000..4cce26aedc
--- /dev/null
+++ b/doc/changelog/02-specification-language/10758-fix-10757.rst
@@ -0,0 +1,5 @@
+- ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes
+  involving ``Prop`` types (`#10758
+  <https://github.com/coq/coq/pull/10758>`_, by Gaëtan Gilbert, fixing
+  `#10757 <https://github.com/coq/coq/issues/10757>`_ reported by
+  Xavier Leroy).
diff --git a/doc/changelog/04-tactics/10765-micromega-caches.rst b/doc/changelog/04-tactics/10765-micromega-caches.rst
new file mode 100644
index 0000000000..12d8f68e63
--- /dev/null
+++ b/doc/changelog/04-tactics/10765-micromega-caches.rst
@@ -0,0 +1,3 @@
+- Introduction of flags :flag:`Lia Cache`, :flag:`Nia Cache` and :flag:`Nra Cache`.
+  (see `#10772 <https://github.com/coq/coq/issues/10772>`_ for use case)
+  (`#10765 <https://github.com/coq/coq/pull/10765>`_ fixes `#10772 <https://github.com/coq/coq/issues/10772>`_ , by Frédéric Besson).
diff --git a/doc/changelog/04-tactics/10774-zify-Z_to_N.rst b/doc/changelog/04-tactics/10774-zify-Z_to_N.rst
new file mode 100644
index 0000000000..ed46cb101e
--- /dev/null
+++ b/doc/changelog/04-tactics/10774-zify-Z_to_N.rst
@@ -0,0 +1,3 @@
+- The :tacn:`zify` tactic is now aware of `Z.to_N`.
+  (`#10774 <https://github.com/coq/coq/pull/10774>`_ fixes
+  `#9162 <https://github.com/coq/coq/issues/9162>`_, by Kazuhiko Sakaguchi).
diff --git a/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst
new file mode 100644
index 0000000000..7babcdb6f1
--- /dev/null
+++ b/doc/changelog/10-standard-library/09772-ordered_type-hint-db.rst
@@ -0,0 +1,4 @@
+-  Moved the `auto` hints of the `OrderedType` module into a new `ordered_type`
+   database
+   (`#9772 <https://github.com/coq/coq/pull/9772>`_,
+   by Vincent Laporte).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 238106b2e7..4a691bde3a 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -35,6 +35,18 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
    use the Simplex method for solving linear goals. If it is not set,
    the decision procedures are using Fourier elimination.
 
+.. flag:: Lia Cache
+
+   This option (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache`
+
+.. flag:: Nia Cache
+
+   This option (set by default) instructs :tacn:`nia` to cache its results in the file `.nia.cache`
+
+.. flag:: Nra Cache
+
+   This option (set by default) instructs :tacn:`nra` to cache its results in the file `.nra.cache`
+
 
 The tactics solve propositional formulas parameterized by atomic
 arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`.
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 7e698bfb66..905068e316 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -147,14 +147,7 @@ Many other commands support the ``Polymorphic`` flag, including:
 - :cmd:`Section` will locally set the polymorphism flag inside the section.
 
 - ``Variables``, ``Context``, ``Universe`` and ``Constraint`` in a section support
-  polymorphism. This means that the universe variables (and associated
-  constraints) are discharged polymorphically over definitions that use
-  them. In other words, two definitions in the section sharing a common
-  variable will both get parameterized by the universes produced by the
-  variable declaration. This is in contrast to a “mononorphic” variable
-  which introduces global universes and constraints, making the two
-  definitions depend on the *same* global universes associated to the
-  variable.
+  polymorphism. See :ref:`universe-polymorphism-in-sections` for more details.
 
 - :cmd:`Hint Resolve` and :cmd:`Hint Rewrite` will use the auto/rewrite hint
   polymorphically, not at a single instance.
@@ -375,9 +368,7 @@ to universes and explicitly instantiate polymorphic definitions.
    as well. Global universe names live in a separate namespace. The
    command supports the ``Polymorphic`` flag only in sections, meaning the
    universe quantification will be discharged on each section definition
-   independently. One cannot mix polymorphic and monomorphic
-   declarations in the same section.
-
+   independently.
 
 .. cmd:: Constraint @universe_constraint
          Polymorphic Constraint @universe_constraint
@@ -510,3 +501,51 @@ underscore or by omitting the annotation to a polymorphic definition.
 
       Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed.
       About baz.
+
+.. _universe-polymorphism-in-sections:
+
+Universe polymorphism and sections
+----------------------------------
+
+:cmd:`Variables`, :cmd:`Context`, :cmd:`Universe` and
+:cmd:`Constraint` in a section support polymorphism. This means that
+the universe variables and their associated constraints are discharged
+polymorphically over definitions that use them. In other words, two
+definitions in the section sharing a common variable will both get
+parameterized by the universes produced by the variable declaration.
+This is in contrast to a “mononorphic” variable which introduces
+global universes and constraints, making the two definitions depend on
+the *same* global universes associated to the variable.
+
+It is possible to mix universe polymorphism and monomorphism in
+sections, except in the following ways:
+
+- no monomorphic constraint may refer to a polymorphic universe:
+
+  .. coqtop:: all reset
+
+     Section Foo.
+
+       Polymorphic Universe i.
+       Fail Constraint i = i.
+
+  This includes constraints implictly declared by commands such as
+  :cmd:`Variable`, which may as a such need to be used with universe
+  polymorphism activated (locally by attribute or globally by option):
+
+  .. coqtop:: all
+
+     Fail Variable A : (Type@{i} : Type).
+     Polymorphic Variable A : (Type@{i} : Type).
+
+  (in the above example the anonymous :g:`Type` constrains polymorphic
+  universe :g:`i` to be strictly smaller.)
+
+- no monomorphic constant or inductive may be declared if polymorphic
+  universes or universe constraints are present.
+
+These restrictions are required in order to produce a sensible result
+when closing the section (the requirement on constants and inductives
+is stricter than the one on constraints, because constants and
+inductives are abstracted by *all* the section's polymorphic universes
+and constraints).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 38b3c34209..0148925247 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -718,6 +718,14 @@ Changes in 8.10+beta3
   follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_,
   which added ``uncons`` in 8.10+beta1).
 
+Changes in 8.10.0
+~~~~~~~~~~~~~~~~~
+
+- Micromega tactics (:tacn:`lia`, :tacn:`nia`, etc) are no longer confused by
+  primitive projections (`#10806 <https://github.com/coq/coq/pull/10806>`_,
+  fixes `#9512 <https://github.com/coq/coq/issues/9512>`_
+  by Vincent Laporte).
+
 Version 8.9
 -----------
 
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index dc4f91e66b..2d047a1058 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -638,7 +638,11 @@ the induction principle to easily reason about the function.
 
    than like this:
 
-   .. coqtop:: reset all
+   .. coqtop:: reset none
+
+      Require Import FunInd.
+
+   .. coqtop:: all
 
       Function plus (n m : nat) {struct n} : nat :=
       match n with
@@ -649,17 +653,22 @@ the induction principle to easily reason about the function.
 
 *Limitations*
 
-|term_0| must be built as a *pure pattern matching tree* (:g:`match … with`)
+:token:`term` must be built as a *pure pattern matching tree* (:g:`match … with`)
 with applications only *at the end* of each branch.
 
 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:: all
+.. coqtop:: none
+
+   Require List.
+   Import List.ListNotations.
+
+.. coqtop:: all fail
 
-   Fail Function wrong (C:nat) : nat :=
-   List.hd 0 (List.map wrong (C::nil)).
+   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.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index fa6d62ffa2..c910136406 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3005,7 +3005,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    flags are either ``beta``, ``delta``, ``match``, ``fix``, ``cofix``,
    ``iota`` or ``zeta``. The ``iota`` flag is a shorthand for ``match``, ``fix``
    and ``cofix``. The ``delta`` flag itself can be refined into
-   :n:`delta {+ @qualid}` or :n:`delta -{+ @qualid}`, restricting in the first
+   :n:`delta [ {+ @qualid} ]` or :n:`delta - [ {+ @qualid} ]`, restricting in the first
    case the constants to unfold to the constants listed, and restricting in the
    second case the constant to unfold to all but the ones explicitly mentioned.
    Notice that the ``delta`` flag does not apply to variables bound by a let-in
@@ -3049,18 +3049,18 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    This is a synonym for ``lazy beta delta iota zeta``.
 
-.. tacv:: compute {+ @qualid}
-          cbv {+ @qualid}
+.. tacv:: compute [ {+ @qualid} ]
+          cbv [ {+ @qualid} ]
 
    These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`.
 
-.. tacv:: compute -{+ @qualid}
-          cbv -{+ @qualid}
+.. tacv:: compute - [ {+ @qualid} ]
+          cbv - [ {+ @qualid} ]
 
    These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`.
 
-.. tacv:: lazy {+ @qualid}
-          lazy -{+ @qualid}
+.. tacv:: lazy [ {+ @qualid} ]
+          lazy - [ {+ @qualid} ]
 
    These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta`
    and :n:`lazy beta delta -{+ @qualid} iota zeta`.
@@ -3071,7 +3071,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
    This tactic evaluates the goal using the optimized call-by-value evaluation
    bytecode-based virtual machine described in :cite:`CompiledStrongReduction`.
    This algorithm is dramatically more efficient than the algorithm used for the
-   ``cbv`` tactic, but it cannot be fine-tuned. It is specially interesting for
+   :tacn:`cbv` tactic, but it cannot be fine-tuned. It is especially interesting for
    full evaluation of algebraic objects. This includes the case of
    reflection-based tactics.
 
@@ -3080,14 +3080,14 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
    This tactic evaluates the goal by compilation to OCaml as described
    in :cite:`FullReduction`. If Coq is running in native code, it can be
-   typically two to five times faster than ``vm_compute``. Note however that the
+   typically two to five times faster than :tacn:`vm_compute`. Note however that the
    compilation cost is higher, so it is worth using only for intensive
    computations.
 
    .. flag:: NativeCompute Profiling
 
       On Linux, if you have the ``perf`` profiler installed, this option makes
-      it possible to profile ``native_compute`` evaluations.
+      it possible to profile :tacn:`native_compute` evaluations.
 
    .. opt:: NativeCompute Profile Filename @string
       :name: NativeCompute Profile Filename
@@ -3097,7 +3097,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
       will contain extra characters to avoid overwriting an existing file; that
       filename is reported to the user.
       That means you can individually profile multiple uses of
-      ``native_compute`` in a script. From the Linux command line, run ``perf report``
+      :tacn:`native_compute` in a script. From the Linux command line, run ``perf report``
       on the profile file to see the results. Consult the ``perf`` documentation
       for more details.
 
@@ -3153,14 +3153,15 @@ the conversion in hypotheses :n:`{+ @ident}`.
      use the name of the constant the (co)fixpoint comes from instead of
      the (co)fixpoint definition in recursive calls.
 
-   The ``cbn`` tactic is claimed to be a more principled, faster and more
-   predictable replacement for ``simpl``.
+   The :tacn:`cbn` tactic is claimed to be a more principled, faster and more
+   predictable replacement for :tacn:`simpl`.
 
-   The ``cbn`` tactic accepts the same flags as ``cbv`` and ``lazy``. The
-   behavior of both ``simpl`` and ``cbn`` can be tuned using the
-   Arguments vernacular command as follows:
+   The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and
+   :tacn:`lazy`. The behavior of both :tacn:`simpl` and :tacn:`cbn`
+   can be tuned using the Arguments vernacular command as follows:
 
-   + A constant can be marked to be never unfolded by ``cbn`` or ``simpl``:
+   + A constant can be marked to be never unfolded by :tacn:`cbn` or
+     :tacn:`simpl`:
 
      .. example::
 
@@ -3169,7 +3170,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
            Arguments minus n m : simpl never.
 
      After that command an expression like :g:`(minus (S x) y)` is left
-     untouched by the tactics ``cbn`` and ``simpl``.
+     untouched by the tactics :tacn:`cbn` and :tacn:`simpl`.
 
    + A constant can be marked to be unfolded only if applied to enough
      arguments. The number of arguments required can be specified using the
@@ -3184,7 +3185,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
            Notation "f \o g" := (fcomp f g) (at level 50).
 
      After that command the expression :g:`(f \o g)` is left untouched by
-     ``simpl`` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`.
+     :tacn:`simpl` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`.
      The same mechanism can be used to make a constant volatile, i.e.
      always unfolded.
 
@@ -3206,7 +3207,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
            Arguments minus !n !m.
 
      After that command, the expression :g:`(minus (S x) y)` is left untouched
-     by ``simpl``, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`.
+     by :tacn:`simpl`, while :g:`(minus (S x) (S y))` is reduced to :g:`(minus x y)`.
 
    + A special heuristic to determine if a constant has to be unfolded
      can be activated with the following command:
@@ -3222,25 +3223,25 @@ the conversion in hypotheses :n:`{+ @ident}`.
      :g:`(minus (S (S x)) (S y))` is simplified to :g:`(minus (S x) y)`
      even if an extra simplification is possible.
 
-   In detail, the tactic ``simpl`` first applies :math:`\beta`:math:`\iota`-reduction. Then, it
+   In detail, the tactic :tacn:`simpl` first applies :math:`\beta`:math:`\iota`-reduction. Then, it
    expands transparent constants and tries to reduce further using :math:`\beta`:math:`\iota`-
    reduction. But, when no :math:`\iota` rule is applied after unfolding then
-   :math:`\delta`-reductions are not applied. For instance trying to use ``simpl`` on
+   :math:`\delta`-reductions are not applied. For instance trying to use :tacn:`simpl` on
    :g:`(plus n O) = n` changes nothing.
 
    Notice that only transparent constants whose name can be reused in the
-   recursive calls are possibly unfolded by ``simpl``. For instance a
+   recursive calls are possibly unfolded by :tacn:`simpl`. For instance a
    constant defined by :g:`plus' := plus` is possibly unfolded and reused in
    the recursive calls, but a constant such as :g:`succ := plus (S O)` is
-   never unfolded. This is the main difference between ``simpl`` and ``cbn``.
-   The tactic ``cbn`` reduces whenever it will be able to reuse it or not:
+   never unfolded. This is the main difference between :tacn:`simpl` and :tacn:`cbn`.
+   The tactic :tacn:`cbn` reduces whenever it will be able to reuse it or not:
    :g:`succ t` is reduced to :g:`S t`.
 
-.. tacv:: cbn {+ @qualid}
-          cbn -{+ @qualid}
+.. tacv:: cbn [ {+ @qualid} ]
+          cbn - [ {+ @qualid} ]
 
-   These are respectively synonyms of :n:`cbn beta delta {+ @qualid} iota zeta`
-   and :n:`cbn beta delta -{+ @qualid} iota zeta` (see :tacn:`cbn`).
+   These are respectively synonyms of :n:`cbn beta delta [ {+ @qualid} ] iota zeta`
+   and :n:`cbn beta delta - [ {+ @qualid} ] iota zeta` (see :tacn:`cbn`).
 
 .. tacv:: simpl @pattern
 
@@ -3249,7 +3250,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 
 .. tacv:: simpl @pattern at {+ @num}
 
-   This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms
+   This applies :tacn:`simpl` only to the :n:`{+ @num}` occurrences of the subterms
    matching :n:`@pattern` in the current goal.
 
    .. exn:: Too few occurrences.
@@ -3265,7 +3266,7 @@ the conversion in hypotheses :n:`{+ @ident}`.
 .. tacv:: simpl @qualid at {+ @num}
           simpl @string at {+ @num}
 
-   This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose
+   This applies :tacn:`simpl` only to the :n:`{+ @num}` applicative subterms whose
    head occurrence is :n:`@qualid` (or :n:`@string`).
 
 .. flag:: Debug RAKAM
@@ -3960,6 +3961,9 @@ At Coq startup, only the core database is nonempty and can be used.
 
 :fset: internal database for the implementation of the ``FSets`` library.
 
+:ordered_type: lemmas about ordered types (as defined in the legacy ``OrderedType`` module),
+               mainly used in the ``FSets`` and ``FMaps`` libraries.
+
 You are advised not to put your own hints in the core database, but
 use one or several databases specific to your development.
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index cc91776a4d..d1b98b94a3 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -515,7 +515,9 @@ through the <tt>Require Import</tt> command.</p>
   <dd>
     theories/Reals/Rdefinitions.v
     theories/Reals/ConstructiveReals.v
+    theories/Reals/ConstructiveRealsMorphisms.v
     theories/Reals/ConstructiveCauchyReals.v
+    theories/Reals/ConstructiveCauchyRealsMult.v
     theories/Reals/Raxioms.v
     theories/Reals/ConstructiveRIneq.v
     theories/Reals/ConstructiveRealsLUB.v