From 8c43e795c772090b336c0f170a6e5dcab196125d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 22 Jun 2018 13:45:03 +0200 Subject: Remove fourier plugin As stated in the manual, the fourier tactic is subsumed by lra. --- doc/sphinx/language/coq-library.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx/language/coq-library.rst') 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 -- cgit v1.2.3