9 files changed, 224 insertions, 29 deletions
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index e0eec2ae2d..323da93f3e 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -617,3 +617,38 @@ the Calculus of Inductive Constructions}},
   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/changes.rst b/doc/sphinx/changes.rst
index e5c2056c40..0f501382e7 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -14,9 +14,9 @@ Version 8.12
 Summary of changes
 ~~~~~~~~~~~~~~~~~~
 
-|Coq| version 8.12 integrates many quality-of-life improvements,
+|Coq| version 8.12 integrates many usability improvements,
 in particular with respect to notations, scopes and implicit arguments,
-along with many bug-fixes and major improvements to the reference manual.
+along with many bug fixes and major improvements to the reference manual.
 The main changes include:
 
 - New :ref:`binder notation<812Implicit>` for non-maximal implicit arguments using :g:`[ ]`
@@ -64,6 +64,23 @@ Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with
 contributions from many users. A list of packages is available at
 https://coq.inria.fr/opam/www/.
 
+Previously, most components of Coq had a single principal maintainer.
+This was changed in 8.12 (`#11295
+<https://github.com/coq/coq/pull/11295>`_) so that every component now has
+a team of maintainers, who are in charge of reviewing and
+merging incoming pull requests.  This gave us a chance to
+significantly expand the pool of maintainters and provide faster
+feedback to contributors.  Special thanks to all our maintainers!
+
+Our current 31 maintainers are Yves Bertot, Frédéric Besson, Tej
+Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès,
+Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert,
+Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin,
+Vincent Laporte, Assia Mahboubi, Kenji Maillard, Guillaume Melquiond,
+Pierre-Marie Pédrot, Clément Pit-Claudel, Kazuhiko Sakaguchi, Vincent
+Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico
+Tassi, Laurent Théry, Anton Trunov, Li-yao Xia, Théo Zimmermann
+
 The 59 contributors to this version are Abhishek Anand, Yves Bertot, Frédéric
 Besson, Lasse Blaauwbroek, Simon Boulier, Quentin Carbonneaux, Tej Chajed,
 Arthur Charguéraud, Cyril Cohen, Pierre Courtieu, Matthew Dempsky, Maxime Dénès,
@@ -72,8 +89,8 @@ Jesús Gallego Arias, Paolo G. Giarrusso, Gaëtan Gilbert, Jason Gross, Samuel
 Gruetter, Attila Gáspár, Hugo Herbelin, Jan-Oliver Kaiser, Robbert Krebbers,
 Vincent Laporte, Olivier Laurent, Xavier Leroy, Thomas Letan, Yishuai Li,
 Kenji Maillard, Erik Martin-Dorel, Guillaume Melquiond, Ike Mulder,
-Guillaume Munch-Maccagnoni, Antonio Nikishaev, Karl Palmskog, Clément
-Pit-Claudel, Pierre-Marie Pédrot, Ramkumar Ramachandra, Lars Rasmusson, Daniel
+Guillaume Munch-Maccagnoni, Antonio Nikishaev, Karl Palmskog, Pierre-Marie
+Pédrot, Clément Pit-Claudel, Ramkumar Ramachandra, Lars Rasmusson, Daniel
 de Rauglaudre, Talia Ringer, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria,
 @scinart, Kartik Singhal, Michael Soegtrop, Matthieu Sozeau, Enrico Tassi,
 Laurent Théry, Ralf Treinen, Anton Trunov, Bernhard M. Wiedemann, Li-yao Xia,
@@ -119,6 +136,18 @@ Specification language, type inference
   :cmd:`Arguments`) has been turned into an error
   (`#11368 <https://github.com/coq/coq/pull/11368>`_,
   by SimonBoulier).
+- **Changed:**
+  Typeclass resolution, accessible through :tacn:`typeclasses eauto`,
+  now suspends constraints according to their modes
+  instead of failing. If a typeclass constraint does not match
+  any of the declared modes for its class, the constraint is postponed, and
+  the proof search continues on other goals. Proof search does a fixed point
+  computation to try to solve them at a later stage of resolution. It does
+  not fail if there remain only stuck constraints at the end of resolution.
+  This makes typeclasses with declared modes more robust with respect to the
+  order of resolution.
+  (`#10858 <https://github.com/coq/coq/pull/10858>`_,
+  fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau).
 - **Added:**
   Warn when manual implicit arguments are used in unexpected positions
   of a term (e.g. in `Check id (forall {x}, x)`) or when an implicit
@@ -1109,6 +1138,84 @@ Infrastructure and dependencies
   (`#11245 <https://github.com/coq/coq/pull/11245>`_,
   by Emilio Jesus Gallego Arias).
 
+Changes in 8.12.0
+~~~~~~~~~~~~~~~~~~~~~
+
+.. contents::
+   :local:
+
+**Notations**
+
+- **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).
+- **Fixed:**
+  Printing bug with notations for n-ary applications used with applied references.
+  (`#12683 <https://github.com/coq/coq/pull/12683>`_,
+  fixes `#12682 <https://github.com/coq/coq/pull/12682>`_,
+  by Hugo Herbelin).
+
+**Tactics**
+
+- **Fixed:**
+  :tacn:`typeclasses eauto` (and discriminated hint bases) now correctly
+  classify local variables as being unfoldable
+  (`#12572 <https://github.com/coq/coq/pull/12572>`_,
+  fixes `#12571 <https://github.com/coq/coq/issues/12571>`_,
+  by Pierre-Marie Pédrot).
+
+**Tactic language**
+
+- **Fixed:**
+  Excluding occurrences was causing an anomaly in tactics
+  (e.g., :g:`pattern _ at L` where :g:`L` is :g:`-2`).
+  (`#12541 <https://github.com/coq/coq/pull/12541>`_,
+  fixes `#12228 <https://github.com/coq/coq/issues/12228>`_,
+  by Pierre Roux).
+- **Fixed:**
+  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).
+
+**SSReflect**
+
+- **Fixed:**
+  Do not store the full environment inside ssr ast_closure_term
+  (`#12708 <https://github.com/coq/coq/pull/12708>`_,
+  fixes `#12707 <https://github.com/coq/coq/issues/12707>`_,
+  by Pierre-Marie Pédrot).
+
+**Commands and options**
+
+- **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).
+- **Changed:**
+  Arbitrary hints have been undeprecated, and their definition
+  now triggers a standard warning instead
+  (`#12678 <https://github.com/coq/coq/pull/12678>`_,
+  fixes `#11970 <https://github.com/coq/coq/issues/11970>`_,
+  by Pierre-Marie Pédrot).
+
+**CoqIDE**
+
+- **Fixed:** CoqIDE no longer exits when trying to open a file whose name is not a valid identifier
+  (`#12562 <https://github.com/coq/coq/pull/12562>`_,
+  fixes `#10988 <https://github.com/coq/coq/issues/10988>`_,
+  by Vincent Laporte).
+
+**Infrastructure and dependencies**
+
+- **Fixed:**
+  Running ``make`` in ``test-suite/`` twice (or more) in a row will no longer
+  rebuild the ``modules/`` tests on subsequent runs, if they have not been
+  modified in the meantime (`#12583 <https://github.com/coq/coq/pull/12583>`_,
+  fixes `#12582 <https://github.com/coq/coq/issues/12582>`_, by Jason Gross).
+
 Version 8.11
 ------------
 
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/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst
index 40e0898871..20f4310d13 100644
--- a/doc/sphinx/language/extensions/evars.rst
+++ b/doc/sphinx/language/extensions/evars.rst
@@ -13,13 +13,13 @@ Existential variables
    | ?[ ?@ident ]
    | ?@ident {? @%{ {+; @ident := @term } %} }
 
-|Coq| terms can include existential variables which represents unknown
-subterms to eventually be replaced by actual subterms.
+|Coq| terms can include existential variables that represent unknown
+subterms that are eventually replaced with actual subterms.
 
-Existential variables are generated in place of unsolvable implicit
+Existential variables are generated in place of unsolved 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
+:tacn:`refine`, as well as in place of unsolved 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,
@@ -43,22 +43,18 @@ existential variable is represented by “?” followed by an identifier.
    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
+outside its context of definition, its instance, written in the
+form :n:`{ {*; @ident := @term} }`, is appended 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.
+Only the variables that are defined in another context are displayed:
+this is why an existential variable used in the same context as its
+context of definition is written with no instance.
+This behaviour may be changed: see :ref:`explicit-display-existentials`.
 
 .. 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.
@@ -88,6 +84,14 @@ Explicit displaying of existential instances for pretty-printing
    context of an existential variable is instantiated at each of the
    occurrences of the existential variable.
 
+.. coqtop:: all
+
+   Check (fun x y => _) 0 1.
+
+   Set Printing Existential Instances.
+
+   Check (fun x y => _) 0 1.
+
 .. _tactics-in-terms:
 
 Solving existential variables using tactics
diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst
index bbd486e3ba..ca69072cb9 100644
--- a/doc/sphinx/language/extensions/implicit-arguments.rst
+++ b/doc/sphinx/language/extensions/implicit-arguments.rst
@@ -70,7 +70,7 @@ is said *contextual* if it can be inferred only from the knowledge of
 the type of the context of the current expression. For instance, the
 only argument of::
 
-  nil : forall A:Set, list A`
+  nil : forall A:Set, list A
 
 is contextual. Similarly, both arguments of a term of type::
 
@@ -539,7 +539,7 @@ with free variables into a closed statement where these variables are
 quantified explicitly.  Use the :cmd:`Generalizable` command to designate
 which variables should be generalized.
 
-It is activated for a binder by prefixing a \`, and for terms by
+It is activated within a binder by prefixing it with \`, and for terms by
 surrounding it with \`{ }, or \`[ ] or \`( ).
 
 Terms surrounded by \`{ } introduce their free variables as maximally
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index b4558ef07f..d6a828521f 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -94,7 +94,7 @@ 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
+constructor.  Then, in :n:`@term__1`, these variables are bound to the
 arguments of the constructor in :n:`@term__0`.  For instance, the
 definition
 
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 7b3670164b..3b4b80ca21 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2280,7 +2280,7 @@ to the others.
 Iteration
 ~~~~~~~~~
 
-.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] }
+.. tacn:: do {? @mult } {| @tactic | [ {+| @tactic } ] }
    :name: do (ssreflect)
 
    This tactical offers an accurate control on the repetition of tactics.
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 fcd5ecc070..18149a690a 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1786,13 +1786,13 @@ Tactic notations allow customizing the syntax of tactics.
 
       * - ``reference``
         - :token:`qualid`
-        - a global reference of term
-        - :tacn:`unfold`
+        - a qualified identifier
+        - name of an |Ltac|-defined tactic
 
       * - ``smart_global``
         - :token:`reference`
         - a global reference of term
-        - :tacn:`with_strategy`
+        - :tacn:`unfold`, :tacn:`with_strategy`
 
       * - ``constr``
         - :token:`term`