14 files changed, 68 insertions, 44 deletions
diff --git a/doc/changelog/01-kernel/11972-fix-require-in-section.rst b/doc/changelog/01-kernel/11972-fix-require-in-section.rst
new file mode 100644
index 0000000000..7a2fa9185f
--- /dev/null
+++ b/doc/changelog/01-kernel/11972-fix-require-in-section.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Using :cmd:`Require` inside a section caused an anomaly when closing
+  the section. (`#11972 <https://github.com/coq/coq/pull/11972>`_, by
+  Gaëtan Gilbert, fixing `#11783
+  <https://github.com/coq/coq/issues/11783>`_, reported by Attila
+  Boros).
diff --git a/doc/changelog/04-tactics/11023-nativecompute-timing.rst b/doc/changelog/04-tactics/11023-nativecompute-timing.rst
deleted file mode 100644
index e8cdfcca21..0000000000
--- a/doc/changelog/04-tactics/11023-nativecompute-timing.rst
+++ /dev/null
@@ -1,7 +0,0 @@
-- The :flag:`NativeCompute Timing` flag causes calls to
-  :tacn:`native_compute` (as well as kernel calls to the native
-  compiler) to emit separate timing information about compilation,
-  execution, and reification.  It replaces the timing information
-  previously emitted when the `-debug` flag was set, and allows more
-  fine-grained timing of the native compiler (`#11023
-  <https://github.com/coq/coq/pull/11023>`_, by Jason Gross).
diff --git a/doc/changelog/04-tactics/11025-nativecompute-timing.rst b/doc/changelog/04-tactics/11025-nativecompute-timing.rst
new file mode 100644
index 0000000000..cb77457c31
--- /dev/null
+++ b/doc/changelog/04-tactics/11025-nativecompute-timing.rst
@@ -0,0 +1,11 @@
+- **Changed:** The :flag:`NativeCompute Timing` flag causes calls to
+  :tacn:`native_compute` (as well as kernel calls to the native
+  compiler) to emit separate timing information about conversion to
+  native code, compilation, execution, and reification.  It replaces
+  the timing information previously emitted when the `-debug` flag was
+  set, and allows more fine-grained timing of the native compiler
+  (`#11025 <https://github.com/coq/coq/pull/11025>`_, by Jason Gross).
+  Additionally, the timing information now uses real time rather than
+  user time (Fixes `#11962
+  <https://github.com/coq/coq/issues/11962>`_, `#11963
+  <https://github.com/coq/coq/pull/11963>`_, by Jason Gross)
diff --git a/doc/changelog/04-tactics/11976-deprecate-omega.rst b/doc/changelog/04-tactics/11976-deprecate-omega.rst
new file mode 100644
index 0000000000..59c9612d17
--- /dev/null
+++ b/doc/changelog/04-tactics/11976-deprecate-omega.rst
@@ -0,0 +1,5 @@
+- **Deprecated:**
+  The :tacn:`omega` tactic is deprecated;
+  use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead
+  (`#11976 <https://github.com/coq/coq/pull/11976>`_,
+  by Vincent Laporte).
diff --git a/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst b/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst
new file mode 100644
index 0000000000..0f30b5f5e8
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Ignore -native-compiler option when built without native compute
+  support.
+  (`#12070 <https://github.com/coq/coq/pull/12070>`_,
+  by Pierre Roux).
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 73d94c2a51..8c2090f3be 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -286,8 +286,8 @@ END
 VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
 | ![ proof_query ] [ "ExploreProof" ] ->
   { fun ~pstate ->
-    let sigma, env = Pfedit.get_current_context pstate in
-    let pprf = Proof.partial_proof (Proof_global.get_proof pstate) in
+    let sigma, env = Declare.get_current_context pstate in
+    let pprf = Proof.partial_proof (Declare.Proof.get_proof pstate) in
     Feedback.msg_notice
       (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
   }
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 8c4dc0e8a6..b94b1fc657 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,8 +1,6 @@
-let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt  =
-  DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook
-    ~opaque ~poly ~udecl ~types:tyopt ~body sigma
-
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
-  edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-    ~kind:Decls.(IsDefinition Definition) ~opaque:false ~impargs:[] ~udecl sigma body None
+  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind = Decls.(IsDefinition Definition) in
+  DeclareDef.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl
+    ~opaque:false ~poly ~types:None ~body sigma
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index f706633da9..77bf58aac6 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -1,4 +1,4 @@
-.. _ micromega:
+.. _micromega:
 
 Micromega: tactics for solving arithmetic goals over ordered rings
 ==================================================================
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index daca43e65e..082ea4691b 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -7,20 +7,18 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic
 
 .. warning::
 
-   The :tacn:`omega` tactic is about to be deprecated in favor of the
-   :tacn:`lia` tactic.  The goal is to consolidate the arithmetic
-   solving capabilities of Coq into a single engine; moreover,
-   :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a
-   complete Presburger arithmetic solver while :tacn:`omega` was known
-   to be incomplete).
-
-   Work is in progress to make sure that there are no regressions
-   (including no performance regression) when switching from
-   :tacn:`omega` to :tacn:`lia` in existing projects.  However, we
-   already recommend using :tacn:`lia` in new or refactored proof
-   scripts.  We also ask that you report (in our `bug tracker
-   <https://github.com/coq/coq/issues>`_) any issue you encounter,
-   especially if the issue was not present in :tacn:`omega`.
+   The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia`
+   tactic.  The goal is to consolidate the arithmetic solving
+   capabilities of Coq into a single engine; moreover, :tacn:`lia` is
+   in general more powerful than :tacn:`omega` (it is a complete
+   Presburger arithmetic solver while :tacn:`omega` was known to be
+   incomplete).
+
+   It is recommended to switch from :tacn:`omega` to :tacn:`lia` in existing
+   projects.  We also ask that you report (in our `bug tracker
+   <https://github.com/coq/coq/issues>`_) any issue you encounter, especially
+   if the issue was not present in :tacn:`omega`.  If no new issues are
+   reported, :tacn:`omega` will be removed soon.
 
    Note that replacing :tacn:`omega` with :tacn:`lia` can break
    non-robust proof scripts which rely on incompleteness bugs of
@@ -31,6 +29,10 @@ Description of ``omega``
 
 .. tacn:: omega
 
+   .. deprecated:: 8.12
+
+      Use :tacn:`lia` instead.
+
    :tacn:`omega` is a tactic for solving goals in Presburger arithmetic,
    i.e. for proving formulas made of equations and inequalities over the
    type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers.
@@ -118,7 +120,7 @@ loaded by
 
 .. example::
 
-  .. coqtop:: all
+  .. coqtop:: all warn
 
      Require Import Omega.
 
diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 0ace9ef5b9..b63ae32311 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -353,7 +353,7 @@ the optional tactic of the ``Hint Rewrite`` command.
 
    .. coqtop:: in reset
 
-      Require Import Omega.
+      Require Import Lia.
 
    .. coqtop:: in
 
@@ -367,7 +367,7 @@ the optional tactic of the ``Hint Rewrite`` command.
 
    .. coqtop:: in
 
-      Hint Rewrite g0 g1 g2 using omega : base1.
+      Hint Rewrite g0 g1 g2 using lia : base1.
 
    .. coqtop:: in
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 62708b01ed..1772362351 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1715,6 +1715,7 @@ performance issue.
 
 .. coqtop:: reset in
 
+   Set Warnings "-omega-is-deprecated".
    Require Import Coq.omega.Omega.
 
    Ltac mytauto := tauto.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 90a991794f..b5d1e8bffd 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2607,7 +2607,7 @@ After the :token:`i_pattern`, a list of binders is allowed.
   .. coqtop:: reset none
 
      From Coq Require Import ssreflect.
-     From Coq Require Import Omega.
+     From Coq Require Import ZArith Lia.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
@@ -2615,7 +2615,7 @@ After the :token:`i_pattern`, a list of binders is allowed.
   .. coqtop:: all
 
      Lemma test : True.
-     have H x (y : nat) : 2 * x + y = x + x + y by omega.
+     have H x (y : nat) : 2 * x + y = x + x + y by lia.
 
 A proof term provided after ``:=`` can mention these bound variables
 (that are automatically introduced with the given names).
@@ -2625,7 +2625,7 @@ with parentheses even if no type is specified:
 
 .. coqtop:: all restart
 
-   have (x) : 2 * x = x + x by omega.
+   have (x) : 2 * x = x + x by lia.
 
 The :token:`i_item` and :token:`s_item` can be used to interpret the asserted
 hypothesis with views (see section :ref:`views_and_reflection_ssr`) or simplify the resulting
@@ -2668,9 +2668,9 @@ context entry name.
      Arguments Sub {_} _ _.
 
      Lemma test n m (H : m + 1 < n) : True.
-     have @i : 'I_n by apply: (Sub m); omega.
+     have @i : 'I_n by apply: (Sub m); lia.
 
-Note that the subterm produced by :tacn:`omega` is in general huge and
+Note that the subterm produced by :tacn:`lia` is in general huge and
 uninteresting, and hence one may want to hide it.
 For this purpose the ``[: name ]`` intro pattern and the tactic
 ``abstract`` (see :ref:`abstract_ssr`) are provided.
@@ -2680,7 +2680,7 @@ For this purpose the ``[: name ]`` intro pattern and the tactic
   .. coqtop:: all abort
 
      Lemma test n m (H : m + 1 < n) : True.
-     have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; omega.
+     have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; lia.
 
   The type of ``pm`` can be cleaned up by its annotation ``(*1*)`` by just
   simplifying it. The annotations are there for technical reasons only.
@@ -2694,7 +2694,7 @@ with have and an explicit term, they must be used as follows:
 
      Lemma test n m (H : m + 1 < n) : True.
      have [:pm] @i : 'I_n := Sub m pm.
-       by omega.
+       by lia.
 
 In this case the abstract constant ``pm`` is assigned by using it in
 the term that follows ``:=`` and its corresponding goal is left to be
@@ -2712,7 +2712,7 @@ makes use of it).
   .. coqtop:: all abort
 
      Lemma test n m (H : m + 1 < n) : True.
-     have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; omega.
+     have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; lia.
 
 Last, notice that the use of intro patterns for abstract constants is
 orthogonal to the transparent flag ``@`` for have.
@@ -2963,7 +2963,7 @@ illustrated in the following example.
 
   .. coqtop:: reset none
 
-     From Coq Require Import ssreflect Omega.
+     From Coq Require Import ssreflect Lia.
      Set Implicit Arguments.
      Unset Strict Implicit.
      Unset Printing Implicit Defensive.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 6a280b74c2..7da453b7af 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -3134,8 +3134,10 @@ the conversion in hypotheses :n:`{+ @ident}`.
    .. flag:: NativeCompute Timing
 
       This flag causes all calls to the native compiler to print
-      timing information for the compilation, execution, and
-      reification phases of native compilation.
+      timing information for the conversion to native code,
+      compilation, execution, and reification phases of native
+      compilation.  Timing is printed in units of seconds of
+      wall-clock time.
 
    .. flag:: NativeCompute Profiling
 
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 67d0b37e81..65c88ed8d5 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -44,6 +44,7 @@ theories/micromega/Refl.v
 theories/micromega/RingMicromega.v
 theories/micromega/Tauto.v
 theories/micromega/VarMap.v
+theories/micromega/ZArith_hints.v
 theories/micromega/ZCoeff.v
 theories/micromega/ZMicromega.v
 theories/micromega/ZifyInst.v