14 files changed, 217 insertions, 6 deletions
diff --git a/doc/changelog/01-kernel/10390-uip.rst b/doc/changelog/01-kernel/10390-uip.rst
new file mode 100644
index 0000000000..dab096d8db
--- /dev/null
+++ b/doc/changelog/01-kernel/10390-uip.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Definitional UIP, only when :flag:`Definitional UIP` is enabled. See
+  documentation of the flag for details.
+  (`#10390 <https://github.com/coq/coq/pull/10390>`_,
+  by Gaëtan Gilbert).
diff --git a/doc/changelog/01-kernel/11604-persistent-arrays.rst b/doc/changelog/01-kernel/11604-persistent-arrays.rst
new file mode 100644
index 0000000000..fbade033d2
--- /dev/null
+++ b/doc/changelog/01-kernel/11604-persistent-arrays.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Built-in support for persistent arrays, which expose a functional
+  interface but are implemented using an imperative data structure, for
+  better performance.
+  (`#11604 <https://github.com/coq/coq/pull/11604>`_,
+  by Maxime Dénès and Benjamin Grégoire, with help from Gaëtan Gilbert).
diff --git a/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst b/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst
new file mode 100644
index 0000000000..bec121836c
--- /dev/null
+++ b/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst
@@ -0,0 +1,8 @@
+- **Fixed:**
+  A loss of definitional equality for declarations obtained through
+  :cmd:`Include` when entering the scope of a :cmd:`Module` or
+  :cmd:`Module Type` was causing :cmd:`Search` not to see the included
+  declarations
+  (`#12537 <https://github.com/coq/coq/pull/12537>`_, fixes `#12525
+  <https://github.com/coq/coq/pull/12525>`_ and `#12647
+  <https://github.com/coq/coq/pull/12647>`_, by Hugo Herbelin).
diff --git a/doc/changelog/03-notations/12523-term-notation-custom.rst b/doc/changelog/03-notations/12523-term-notation-custom.rst
new file mode 100644
index 0000000000..1a611f3fb1
--- /dev/null
+++ b/doc/changelog/03-notations/12523-term-notation-custom.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Simultaneous definition of terms and notations now support custom entries.
+  Fixes `#11121 <https://github.com/coq/coq/pull/11121>`_.
+  (`#12523 <https://github.com/coq/coq/pull/11523>`_, by Maxime Dénès).
diff --git a/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst
new file mode 100644
index 0000000000..555020d319
--- /dev/null
+++ b/doc/changelog/05-tactic-language/12594-fix-ltac2-type-params.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Fix the parsing of multi-parameters Ltac2 types
+  (`#12594 <https://github.com/coq/coq/pull/12594>`_,
+  fixes `#12595 <https://github.com/coq/coq/issues/12595>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst
new file mode 100644
index 0000000000..c654ddd69d
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12677-require-v811-error-compat.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Properly report the mismatched magic number of vo files
+  (`#12677 <https://github.com/coq/coq/pull/12677>`_,
+  fixes `#12513 <https://github.com/coq/coq/issues/12513>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/08-tools/12613-coqchk-noi.rst b/doc/changelog/08-tools/12613-coqchk-noi.rst
new file mode 100644
index 0000000000..b83c9c69a2
--- /dev/null
+++ b/doc/changelog/08-tools/12613-coqchk-noi.rst
@@ -0,0 +1,3 @@
+- **Removed:** The option ``-I`` of coqchk was removed (it was
+  deprecated in Coq 8.8) (`#12613
+  <https://github.com/coq/coq/pull/12613>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index b19239ed22..6c62ff3116 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -173,6 +173,79 @@ strict propositions. For instance:
   Definition eq_true_is_true b (H:true=b) : is_true b
     := match H in _ = x return is_true x with eq_refl => stt end.
 
+Definitional UIP
+----------------
+
+.. flag:: Definitional UIP
+
+   This flag, off by default, allows the declaration of non-squashed
+   inductive types with 1 constructor which takes no argument in
+   |SProp|. Since this includes equality types, it provides
+   definitional uniqueness of identity proofs.
+
+   Because squashing is a universe restriction, unsetting
+   :flag:`Universe Checking` is stronger than setting
+   :flag:`Definitional UIP`.
+
+Definitional UIP involves a special reduction rule through which
+reduction depends on conversion. Consider the following code:
+
+.. coqtop:: in
+
+   Set Definitional UIP.
+
+   Inductive seq {A} (a:A) : A -> SProp :=
+     srefl : seq a a.
+
+   Axiom e : seq 0 0.
+   Definition hidden_arrow := match e return Set with srefl _ => nat -> nat end.
+
+   Check (fun (f : hidden_arrow) (x:nat) => (f : nat -> nat) x).
+
+By the usual reduction rules :g:`hidden_arrow` is a stuck match, but
+by proof irrelevance :g:`e` is convertible to :g:`srefl 0` and then by
+congruence :g:`hidden_arrow` is convertible to `nat -> nat`.
+
+The special reduction reduces any match on a type which uses
+definitional UIP when the indices are convertible to those of the
+constructor. For `seq`, this means a match on a value of type `seq x
+y` reduces if and only if `x` and `y` are convertible.
+
+Such matches are indicated in the printed representation by inserting
+a cast around the discriminee:
+
+.. coqtop:: out
+
+   Print hidden_arrow.
+
+Non Termination with UIP
+++++++++++++++++++++++++
+
+The special reduction rule of UIP combined with an impredicative sort
+breaks termination of reduction
+:cite:`abel19:failur_normal_impred_type_theor`:
+
+.. coqtop:: all
+
+   Axiom all_eq : forall (P Q:Prop), P -> Q -> seq P Q.
+
+   Definition transport (P Q:Prop) (x:P) (y:Q) : Q
+   := match all_eq P Q x y with srefl _ => x end.
+
+   Definition top : Prop := forall P : Prop, P -> P.
+
+   Definition c : top :=
+     fun P p =>
+     transport
+     (top -> top)
+     P
+     (fun x : top => x (top -> top) (fun x => x) x)
+     p.
+
+   Fail Timeout 1 Eval lazy in c (top -> top) (fun x => x) c.
+
+The term :g:`c (top -> top) (fun x => x) c` infinitely reduces to itself.
+
 Issues with non-cumulativity
 ----------------------------
 
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index 3d73f9bd6e..323da93f3e 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -608,3 +608,47 @@ the Calculus of Inductive Constructions}},
  publisher = {ACM},
  address = {New York, NY, USA},
 }
+
+@techreport{abel19:failur_normal_impred_type_theor,
+  author       = {Andreas Abel AND Thierry Coquand},
+  title        = {{Failure of Normalization in Impredicative Type
+                  Theory with Proof-Irrelevant Propositional
+                  Equality}},
+  year         = 2019,
+  institution = {Chalmers and Gothenburg University},
+}
+
+@inproceedings{ConchonFilliatre07wml,
+  author = {Sylvain Conchon and Jean-Christophe Filliâtre},
+  title = {A Persistent Union-Find Data Structure},
+  booktitle = {ACM SIGPLAN Workshop on ML},
+  publisher = {ACM Press},
+  pages = {37--45},
+  year = 2007,
+  address = {Freiburg, Germany},
+  month = {October},
+  topics = {team, lri},
+  type_publi = {icolcomlec},
+  type_digiteo = {conf_isbn},
+  x-pdf = {https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf},
+  url = {https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf},
+  abstract = { The problem of disjoint sets, also known as union-find,
+  consists in maintaining a partition of a finite set within a data
+  structure. This structure provides two operations: a function find
+  returning the class of an element and a function union merging two
+  classes. An optimal and imperative solution is known since 1975.
+  However, the imperative nature of this data structure may be a
+  drawback when it is used in a backtracking algorithm. This paper
+  details the implementation of a persistent union-find data structure
+  as efficient as its imperative counterpart.  To achieve this result,
+  our solution makes heavy use of imperative features and thus it is a
+  significant example of a data structure whose side effects are
+  safely hidden behind a persistent interface.  To strengthen this
+  last claim, we also detail a formalization using the Coq proof
+  assistant which shows both the correctness of our solution and its
+  observational persistence. },
+  x-equipes = {demons PROVAL},
+  x-type = {article},
+  x-support = {actes_aux},
+  x-cle-support = {ML}
+}
diff --git a/doc/sphinx/language/core/primitive.rst b/doc/sphinx/language/core/primitive.rst
index dc8f131209..727177b23a 100644
--- a/doc/sphinx/language/core/primitive.rst
+++ b/doc/sphinx/language/core/primitive.rst
@@ -40,9 +40,8 @@ These primitive declarations are regular axioms. As such, they must be trusted a
 
    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 reduction machines 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`
@@ -105,3 +104,53 @@ 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)`.
+
+.. _primitive-arrays:
+
+Primitive Arrays
+----------------
+
+The language of terms features persistent arrays as values. The type of
+such a value is *axiomatized*; it is declared through the following sentence
+(excerpt from the :g:`PArray` module):
+
+.. coqdoc::
+
+   Primitive array := #array_type.
+
+This type is equipped with a few operators, that must be similarly declared.
+For instance, elements in an array can be accessed and updated using the
+:g:`PArray.get` and :g:`PArray.set` functions, declared and specified as
+follows:
+
+.. coqdoc::
+
+   Primitive get := #array_get.
+   Primitive set := #array_set.
+   Notation "t .[ i ]" := (get t i).
+   Notation "t .[ i <- a ]" := (set t i a).
+
+   Axiom get_set_same : forall A t i (a:A), (i < length t) = true -> t.[i<-a].[i] = a.
+   Axiom get_set_other : forall A t i j (a:A), i <> j -> t.[i<-a].[j] = t.[j].
+
+The complete set of such operators can be obtained looking at the :g:`PArray` module.
+
+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.
+
+The extraction of these primitives can be customized similarly to the extraction
+of regular axioms (see :ref:`extraction`). Nonetheless, the :g:`ExtrOCamlPArray`
+module can be used when extracting to OCaml: it maps the Coq primitives to types
+and functions of a :g:`Parray` 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 (see ``kernel/parray.ml``).
+
+Primitive arrays expose a functional interface, but they are internally
+implemented using a persistent data structure :cite:`ConchonFilliatre07wml`.
+Update and access to an element in the most recent copy of an array are
+constant time operations.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 4af3ebc47b..25c4de7389 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4162,7 +4162,7 @@ Hint locality
 Hints provided by the ``Hint`` commands are erased when closing a section.
 Conversely, all hints of a module ``A`` that are not defined inside a
 section (and not defined with option ``Local``) become available when the
-module ``A`` is imported (using e.g. ``Require Import A.``).
+module ``A`` is required (using e.g. ``Require A.``).
 
 As of today, hints only have a binary behavior regarding locality, as
 described above: either they disappear at the end of a section scope,
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 3c92206fd2..fcd5ecc070 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -368,13 +368,14 @@ a :token:`decl_notations` clause after the definition of the (co)inductive type
 (co)recursive term (or after the definition of each of them in case of mutual
 definitions). The exact syntax is given by :n:`@decl_notation` for inductive,
 co-inductive, recursive and corecursive definitions and in :ref:`record-types`
-for records.
+for records. Note that only syntax modifiers that do not require to add or
+change a parsing rule are accepted.
 
    .. insertprodn decl_notations decl_notation
 
    .. prodn::
       decl_notations ::= where @decl_notation {* and @decl_notation }
-      decl_notation ::= @string := @one_term {? ( only parsing ) } {? : @scope_name }
+      decl_notation ::= @string := @one_term {? ( {+, @syntax_modifier } ) } {? : @scope_name }
 
 Here are examples:
 
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 4badb20295..f39c50238a 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -15,6 +15,7 @@ theories/extraction/ExtrOcamlBigIntConv.v
 theories/extraction/ExtrOcamlChar.v
 theories/extraction/ExtrOCamlInt63.v
 theories/extraction/ExtrOCamlFloats.v
+theories/extraction/ExtrOCamlPArray.v
 theories/extraction/ExtrOcamlIntConv.v
 theories/extraction/ExtrOcamlNatBigInt.v
 theories/extraction/ExtrOcamlNatInt.v
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index ab615d5f65..7c1328916b 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -709,4 +709,11 @@ through the <tt>Require Import</tt> command.</p>
     theories/Compat/Coq812.v
     theories/Compat/Coq813.v
   </dd>
+
+  <dt> <b>Array</b>:
+    Persistent native arrays
+  </dt>
+  <dd>
+    theories/Array/PArray.v
+  </dd>
 </dl>