Remove fourier plugin

As stated in the manual, the fourier tactic is subsumed by lra.

3 files changed, 7 insertions, 23 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 0e9c23b9b..2407a9051 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -96,15 +96,14 @@ and checked to be :math:`-1`.
 .. tacn:: lra
    :name: lra
 
-This tactic is searching for *linear* refutations using Fourier
-elimination [#]_. As a result, this tactic explores a subset of the *Cone*
-defined as
+   This tactic is searching for *linear* refutations using Fourier
+   elimination [#]_. As a result, this tactic explores a subset of the *Cone*
+   defined as
 
-  :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}`
+   :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}`
 
-The deductive power of `lra` is the combined deductive power of
-`ring_simplify` and `fourier`. There is also an overlap with the field
-tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`.
+   The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field`
+   tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`.
 
 
 `lia`: a tactic for linear integer arithmetic
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index afb49413d..f23e04c3a 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -889,7 +889,7 @@ Notation          Interpretation
 Some tactics for real numbers
 +++++++++++++++++++++++++++++
 
-In addition to the powerful ``ring``, ``field`` and ``fourier``
+In addition to the powerful ``ring``, ``field`` and ``lra``
 tactics (see Chapter :ref:`tactics`), there are also:
 
 .. tacn:: discrR
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index ec085a71e..562f8568d 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -4319,21 +4319,6 @@ printed with the Print Fields command.
 See also: file plugins/setoid_ring/RealField.v for an example of instantiation,
 theory theories/Reals for many examples of use of field.
 
-.. tacn:: fourier
-   :name: fourier
-
-This tactic written by Loïc Pottier solves linear inequalities on real
-numbers using Fourier’s method :cite:`Fourier`. This tactic must be loaded by
-``Require Import Fourier``.
-
-.. example::
-   .. coqtop:: reset all
-
-      Require Import Reals.
-      Require Import Fourier.
-      Goal forall x y:R, (x < y)%R -> (y + 1 >= x - 1)%R.
-      intros; fourier.
-
 Non-logical tactics
 ------------------------