4 files changed, 36 insertions, 3 deletions
diff --git a/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst
new file mode 100644
index 0000000000..2a341261e5
--- /dev/null
+++ b/doc/changelog/04-tactics/11474-lia-bug-fix-11436.rst
@@ -0,0 +1,9 @@
+- **Added:**
+  :cmd:`Show Lia Profile` prints some statistics about :tacn:`lia` calls.
+  (`#11474 <https://github.com/coq/coq/pull/11474>`_,  by Frédéric Besson).
+
+- **Fixed:**
+  Efficiency regression of ``lia``
+  (`#11474 <https://github.com/coq/coq/pull/11474>`_,
+  fixes `#11436 <https://github.com/coq/coq/issues/11436>`_,
+  by Frédéric Besson).
diff --git a/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst
new file mode 100644
index 0000000000..6294cdb24a
--- /dev/null
+++ b/doc/changelog/09-coqide/11414-remove-ide-tactic-menu.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+  Removed the "Tactic" menu from CoqIDE which had been unmaintained for a number of years
+  (`#11414 <https://github.com/coq/coq/pull/11414>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index cc19c8b6a9..b0197c500c 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -35,6 +35,12 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
    use the Simplex method for solving linear goals. If it is not set,
    the decision procedures are using Fourier elimination.
 
+.. cmd:: Show Lia Profile
+
+   This command prints some statistics about the amount of pivoting
+   operations needed by :tacn:`lia` and may be useful to detect
+   inefficiencies (only meaningful if flag :flag:`Simplex` is set).
+
 .. flag:: Lia Cache
 
    This flag (set by default) instructs :tacn:`lia` to cache its results in the file `.lia.cache`
diff --git a/doc/tools/coqrst/checkdeps.py b/doc/tools/coqrst/checkdeps.py
index 91f0a7cb1b..feafcba026 100644
--- a/doc/tools/coqrst/checkdeps.py
+++ b/doc/tools/coqrst/checkdeps.py
@@ -10,13 +10,20 @@
 from __future__ import print_function
 import sys
 
+missing_deps = []
+
 def eprint(*args, **kwargs):
     print(*args, file=sys.stderr, **kwargs)
 
 def missing_dep(dep):
-    eprint('Cannot find %s (needed to build documentation)' % dep)
-    eprint('You can run `pip3 install %s` to install it.' % dep)
-    sys.exit(1)
+    missing_deps.append(dep)
+
+def report_missing_deps():
+    if len(missing_deps) > 0:
+        deps = " ".join(missing_deps)
+        eprint('Cannot find package(s) `%s` (needed to build documentation)' % deps)
+        eprint('You can run `pip3 install %s` to install it/them.' % deps)
+        sys.exit(1)
 
 try:
     import sphinx_rtd_theme
@@ -37,3 +44,10 @@ try:
     import bs4
 except:
     missing_dep('beautifulsoup4')
+
+try:
+    import sphinxcontrib.bibtex
+except:
+    missing_dep('sphinxcontrib-bibtex')
+
+report_missing_deps()