Merge PR #12797: [refman] Take large chunks out of the tactics chapter.

Reviewed-by: jfehrle

4 files changed, 5 insertions, 5 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 0942a82d6f..2c7b637a42 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -1,6 +1,6 @@
 .. _micromega:
 
-Micromega: tactics for solving arithmetic goals over ordered rings
+Micromega: solvers for arithmetic goals over ordered rings
 ==================================================================
 
 :Authors: Frédéric Besson and Evgeny Makarov
diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst
index 85e0cb9536..7a2be3dcef 100644
--- a/doc/sphinx/addendum/nsatz.rst
+++ b/doc/sphinx/addendum/nsatz.rst
@@ -1,6 +1,6 @@
 .. _nsatz_chapter:
 
-Nsatz: tactics for proving equalities in integral domains
+Nsatz: a solver for equalities in integral domains
 ===========================================================
 
 :Author: Loïc Pottier
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 35f087d47d..5c08bc44df 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -1,6 +1,6 @@
 .. _omega_chapter:
 
-Omega: a solver for quantifier-free problems in Presburger Arithmetic
+Omega: a (deprecated) solver for arithmetic
 =====================================================================
 
 :Author: Pierre Crégut
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index da1a393b4a..027db9f47a 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -10,8 +10,8 @@
 
 .. _theringandfieldtacticfamilies:
 
-The ring and field tactic families
-====================================
+ring and field: solvers for polynomial and rational equations
+=============================================================
 
 :Author: Bruno Barras, Benjamin Grégoire, Assia Mahboubi, Laurent Théry [#f1]_