diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-18 17:21:01 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-18 17:21:01 +0200 |
| commit | 8271b23dd0a26bba79c7d6dadd92d2329945675c (patch) | |
| tree | 6d6b4faeda0fc272c1faaa7912406097ef055caa /doc/sphinx/proof-engine/tactics.rst | |
| parent | e5e3725fab9daa810a4c8a383886f1c5dc980e85 (diff) | |
| parent | 8c43e795c772090b336c0f170a6e5dcab196125d (diff) | |
Merge PR #7897: Remove fourier plugin
Diffstat (limited to 'doc/sphinx/proof-engine/tactics.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 15 |
1 files changed, 0 insertions, 15 deletions
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 ------------------------ |