Change the title of the automatic tactic chapter and of its sections.

Prefer the term 'solver' to 'decision procedure'.

5 files changed, 9 insertions, 9 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]_
 
diff --git a/doc/sphinx/proofs/automatic-tactics/index.rst b/doc/sphinx/proofs/automatic-tactics/index.rst
index fa0b0e51af..c3712b109d 100644
--- a/doc/sphinx/proofs/automatic-tactics/index.rst
+++ b/doc/sphinx/proofs/automatic-tactics/index.rst
@@ -1,13 +1,13 @@
 .. _automatic-tactics:
 
 =====================================================
-Built-in decision procedures and programmable tactics
+Automatic solvers and programmable tactics
 =====================================================
 
 Some tactics are largely automated and are able to solve complex
-goals.  This chapter presents both some decision procedures that can
-be used to solve some specific categories of goals, and some
-programmable tactics, that the user can instrument to handle some
+goals.  This chapter presents both built-in solvers that can
+be used on specific categories of goals and
+programmable tactics that the user can instrument to handle
 complex goals in new domains.
 
 .. toctree::