Adding documentation for the move of sections data to kernel.

3 files changed, 40 insertions, 11 deletions

diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index d00c8cb11a..78d7061259 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -129,6 +129,18 @@ Universes
   GH issue number: #9294
   risk: moderate risk to be activated by chance
 
+  component: universe polymorphism, asynchronous proofs
+  summary: universe constraints erroneously discarded when forcing an asynchronous proof containing delayed monomorphic constraints inside a universe polymorphic section
+  introduced: between 8.4 and 8.5 by merging the asynchronous proofs feature branch and universe polymorphism one
+  impacted released: V8.5-V8.10
+  impacted development branches: none
+  impacted coqchk versions: immune
+  fixed in: PR#10664
+  found by: Pédrot
+  exploit: no test
+  GH issue number: none
+  risk: unlikely to be triggered in interactive mode, not present in batch mode (i.e. coqc)
+
 Primitive projections
 
   component: primitive projections, guard condition
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/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 7e698bfb66..1d0b732e7d 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,23 @@ 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
+----------------------------------
+
+The universe polymorphic or monomorphic status is
+attached to each individual section, and all term or universe declarations
+contained inside must respect it, as described below. It is possible to nest a
+polymorphic section inside a monomorphic one, but the converse is not allowed.
+
+: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.