12 files changed, 150 insertions, 34 deletions
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 4df284d2d9..1d0aca1caf 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -145,10 +145,12 @@ END
   it gives an error message that is basically impossible to understand. *)
 
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
-| [ "Cmd9" ] ->
-  { let p = Proof_global.give_me_the_proof () in
-    let sigma, env = Pfedit.get_current_context () in
-    let pprf = Proof.partial_proof p in
-    Feedback.msg_notice
-      (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) }
+| ![ proof ] [ "Cmd9" ] ->
+  { fun ~pstate ->
+    Option.iter (fun (pstate : Proof_global.t) ->
+        let sigma, env = Pfedit.get_current_context pstate in
+        let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in
+        Feedback.msg_notice
+          (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) pstate;
+    pstate }
 END
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index e370d37fc4..23f8fbe888 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,5 +1,5 @@
 (* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *)
-let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
+let edeclare ?hook ~ontop ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
   let sigma = Evd.minimize_universes sigma in
   let body = EConstr.to_constr sigma body in
   let tyopt = Option.map (EConstr.to_constr sigma) tyopt in
@@ -13,13 +13,13 @@ let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
   let ubinders = Evd.universe_binders sigma in
   let ce = Declare.definition_entry ?types:tyopt ~univs body in
   let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-  DeclareDef.declare_definition ident k ce ubinders imps ?hook_data
+  DeclareDef.declare_definition ~ontop ident k ce ubinders imps ?hook_data
 
 let packed_declare_definition ~poly ident value_with_constraints =
   let body, ctx = value_with_constraints in
   let sigma = Evd.from_ctx ctx in
   let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in
   let udecl = UState.default_univ_decl in
-  ignore (edeclare ident k ~opaque:false sigma udecl body None [])
+  ignore (edeclare ~ontop:None ident k ~opaque:false sigma udecl body None [])
 
 (* But this definition cannot be undone by Reset ident *)
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst
index a9d894cab5..dd21ea09bd 100644
--- a/doc/sphinx/addendum/canonical-structures.rst
+++ b/doc/sphinx/addendum/canonical-structures.rst
@@ -92,7 +92,7 @@ and use the ``==`` notation on terms of this type.
 Derived Canonical Structures
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-We know how to use ``== `` on base types, like ``nat``, ``bool``, ``Z``. Here we show
+We know how to use ``==`` on base types, like ``nat``, ``bool``, ``Z``. Here we show
 how to deal with type constructors, i.e. how to make the following
 example work:
 
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 795fccbf08..d5523e8561 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -154,8 +154,10 @@ Declaring Coercions
   .. warn:: Ambiguous path.
 
      When the coercion :token:`qualid` is added to the inheritance graph,
-     invalid coercion paths are ignored; they are signaled by a warning
-     displaying these paths of the form :g:`[f₁;..;fₙ] : C >-> D`.
+     invalid coercion paths are ignored. The :cmd:`Coercion` command tries to check
+     that they are convertible with existing ones on the same classes.
+     The paths for which this check fails are displayed by a warning in the form
+     :g:`[f₁;..;fₙ] : C >-> D`.
 
   .. cmdv:: Local Coercion @qualid : @class >-> @class
 
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 20e4c6a3d6..3b350d5dc0 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -323,7 +323,7 @@ The syntax for adding a new ring is
    decidable :n:`@term`
       declares the ring as computational. The expression
       :n:`@term` is the correctness proof of an equality test ``?=!``
-      (which  hould be evaluable). Its type should be of the form
+      (which should be evaluable). Its type should be of the form
       ``forall x y, x ?=! y = true → x == y``.
 
    morphism :n:`@term`
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index e6a5b3972c..b069cf27f4 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -561,6 +561,8 @@ Settings
 
 .. flag:: Refine Instance Mode
 
+   .. deprecated:: 8.10
+
    This flag allows to switch the behavior of instance declarations made through
    the Instance command.
 
@@ -573,18 +575,19 @@ Settings
 Typeclasses eauto `:=`
 ~~~~~~~~~~~~~~~~~~~~~~
 
-.. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth
+.. cmd:: Typeclasses eauto := {? debug} {? (dfs) | (bfs) } @num
    :name: Typeclasses eauto
 
    This command allows more global customization of the typeclass
    resolution tactic. The semantics of the options are:
 
-   + ``debug`` In debug mode, the trace of successfully applied tactics is
-     printed.  This value can also be set with :flag:`Typeclasses Debug`.
+   + ``debug`` This sets the debug mode. In debug mode, the trace of
+     successfully applied tactics is printed. The debug mode can also
+     be set with :flag:`Typeclasses Debug`.
 
-   + ``dfs, bfs`` This sets the search strategy to depth-first search (the
-     default) or breadth-first search.  This value can also be set with
-     :flag:`Typeclasses Iterative Deepening`.
+   + ``(dfs)``, ``(bfs)`` This sets the search strategy to depth-first
+     search (the default) or breadth-first search. The search strategy
+     can also be set with :flag:`Typeclasses Iterative Deepening`.
 
-   + ``depth`` This sets the depth limit of the search.  This value can also be set with
-     :opt:`Typeclasses Depth`.
+   + :token:`num` This sets the depth limit of the search. The depth
+     limit can also be set with :opt:`Typeclasses Depth`.
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 7c78e1a50f..8346b72cb9 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -34,9 +34,16 @@ For example, to statically link |Ltac|, you can just do:
 
 and similarly for other plugins.
 
+Building a |Coq| project
+------------------------
+
+As of today it is possible to build Coq projects using two tools:
+
+- coq_makefile, which is distributed by Coq and is based on generating a makefile,
+- Dune, the standard OCaml build tool, which, since version 1.9, supports building Coq libraries.
 
 Building a |Coq| project with coq_makefile
-------------------------------------------
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The majority of |Coq| projects are very similar: a collection of ``.v``
 files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of
@@ -119,7 +126,7 @@ distinct plugins because of a clash in their auxiliary module names.
 .. _coqmakefilelocal:
 
 CoqMakefile.local
-~~~~~~~~~~~~~~~~~
++++++++++++++++++
 
 The optional file ``CoqMakefile.local`` is included by the generated
 file ``CoqMakefile``. It can contain two kinds of directives.
@@ -205,7 +212,7 @@ The following makefile rules can be extended.
   target.
 
 Timing targets and performance testing
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+++++++++++++++++++++++++++++++++++++++
 
 The generated ``Makefile`` supports the generation of two kinds of timing
 data: per-file build-times, and per-line times for an individual file.
@@ -385,7 +392,7 @@ line timing data:
 
 
 Reusing/extending the generated Makefile
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+++++++++++++++++++++++++++++++++++++++++
 
 Including the generated makefile with an include directive is
 discouraged. The contents of this file, including variable names and
@@ -429,7 +436,7 @@ have a generic target for invoking unknown targets.
 
 
 Building a subset of the targets with ``-j``
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+++++++++++++++++++++++++++++++++++++++++++++
 
 To build, say, two targets foo.vo and bar.vo in parallel one can use
 ``make only TGTS="foo.vo bar.vo" -j``.
@@ -452,11 +459,90 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use
 
 
 
-Module dependencies
---------------------
+Building a |Coq| project with Dune
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. note::
+
+   The canonical documentation for the Coq Dune extension is
+   maintained upstream; please refer to the `Dune manual
+   <https://dune.readthedocs.io/>`_ for up-to-date information.
+
+Building a Coq project with Dune requires setting up a Dune project
+for your files. This involves adding a ``dune-project`` and
+``pkg.opam`` file to the root (``pkg.opam`` can be empty), and then
+providing ``dune`` files in the directories your ``.v`` files are
+placed. For the experimental version "0.1" of the Coq Dune language,
+|Coq| library stanzas look like:
+
+.. code:: scheme
 
-In order to compute module dependencies (so to use ``make``), |Coq| comes
-with an appropriate tool, ``coqdep``.
+    (coqlib
+     (name <module_prefix>)
+     (public_name <package.lib_name>)
+     (synopsis <text>)
+     (modules <ordered_set_lang>)
+     (libraries <ocaml_libraries>)
+     (flags <coq_flags>))
+
+This stanza will build all `.v` files in the given directory, wrapping
+the library under ``<module_prefix>``. If you declare a
+``<package.lib_name>`` a ``.install`` file for the library will be
+generated; the optional ``<modules>`` field allows you to filter
+the list of modules, and ``<libraries>`` allows to depend on ML
+plugins. For the moment, Dune relies on Coq's standard mechanisms
+(such as ``COQPATH``) to locate installed Coq libraries.
+
+By default Dune will skip ``.v`` files present in subdirectories. In
+order to enable the usual recursive organization of Coq projects add
+
+.. code:: scheme
+
+    (include_subdirs qualified)
+
+to you ``dune`` file.
+
+Once your project is set up, `dune build` will generate the
+`pkg.install` files and all the files necessary for the installation
+of your project.
+
+.. example::
+
+   A typical stanza for a Coq plugin is split into two parts. An OCaml build directive, which is standard Dune:
+
+   .. code:: scheme
+
+       (library
+        (name equations_plugin)
+        (public_name equations.plugin)
+        (flags :standard -warn-error -3-9-27-32-33-50)
+        (libraries coq.plugins.cc coq.plugins.extraction))
+
+       (rule
+        (targets g_equations.ml)
+        (deps (:pp-file g_equations.mlg))
+        (action (run coqpp %{pp-file})))
+
+   And a Coq-specific part that depends on it via the ``libraries`` field:
+
+   .. code:: scheme
+
+       (coqlib
+        (name Equations) ; -R flag
+        (public_name equations.Equations)
+        (synopsis "Equations Plugin")
+        (libraries coq.plugins.extraction equations.plugin)
+        (modules :standard \ IdDec NoCycle)) ; exclude some modules that don't build
+
+       (include_subdirs qualified)
+
+.. _coqdep:
+
+Computing Module dependencies
+-----------------------------
+
+In order to compute module dependencies (to be used by ``make`` or
+``dune``), |Coq| provides the ``coqdep`` tool.
 
 ``coqdep`` computes inter-module dependencies for |Coq| and |OCaml|
 programs, and prints the dependencies on the standard output in a
@@ -474,10 +560,8 @@ done approximately and you are advised to use ``ocamldep`` instead for the
 
 See the man page of ``coqdep`` for more details and options.
 
-The build infrastructure generated by ``coq_makefile`` uses ``coqdep`` to
-automatically compute the dependencies among the files part of the
-project.
-
+Both Dune and ``coq_makefile`` use ``coqdep`` to compute the
+dependencies among the files part of a Coq project.
 
 .. _coqdoc:
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 52e3029b8f..0322b43694 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1071,6 +1071,16 @@ Proving a subgoal as a separate lemma
    It may be useful to generate lemmas minimal w.r.t. the assumptions they
    depend on. This can be obtained thanks to the option below.
 
+   .. warning::
+
+      The abstract tactic, while very useful, still has some known
+      limitations, see https://github.com/coq/coq/issues/9146 for more
+      details. Thus we recommend using it caution in some
+      "non-standard" contexts. In particular, ``abstract`` won't
+      properly work when used inside quotations ``ltac:(...)``, or
+      if used as part of typeclass resolution, it may produce wrong
+      terms when in universe polymorphic mode.
+
    .. tacv:: abstract @expr using @ident
 
       Give explicitly the name of the auxiliary lemma.
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 07215a0c7e..16b158c397 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -544,6 +544,10 @@ Requesting information
 
       ``<Your Tactic Text here>``.
 
+     .. deprecated:: 8.10
+
+        Please use a text editor.
+
    .. cmdv:: Show Proof
       :name: Show Proof
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 7b395900e9..afb0239be4 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3912,6 +3912,8 @@ At Coq startup, only the core database is nonempty and can be used.
                       environment, including those used for ``setoid_rewrite``,
                       from the Classes directory.
 
+:fset: internal database for the implementation of the ``FSets`` library.
+
 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/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index e5eb7eb4f5..1e201953b3 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1473,6 +1473,10 @@ Numeral notations
      :n:`@ident__2` to the number will be fully reduced, and universes
      of the resulting term will be refreshed.
 
+     Note that only fully-reduced ground terms (terms containing only
+     function application, constructors, inductive type families, and
+     primitive integers) will be considered for printing.
+
    .. cmdv:: Numeral Notation @ident__1 @ident__2 @ident__3 : @scope (warning after @num).
 
      When a literal larger than :token:`num` is parsed, a warning
@@ -1618,6 +1622,10 @@ String notations
      :n:`@ident__2` to the string will be fully reduced, and universes
      of the resulting term will be refreshed.
 
+     Note that only fully-reduced ground terms (terms containing only
+     function application, constructors, inductive type families, and
+     primitive integers) will be considered for printing.
+
    .. exn:: Cannot interpret this string as a value of type @type
 
      The string notation registered for :token:`type` does not support
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index b58148ffff..b25104ddb9 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -22,6 +22,7 @@ plugins/extraction/Extraction.v
 plugins/funind/FunInd.v
 plugins/funind/Recdef.v
 plugins/ltac/Ltac.v
+plugins/micromega/DeclConstant.v
 plugins/micromega/Env.v
 plugins/micromega/EnvRing.v
 plugins/micromega/Fourier.v