From 8c43e795c772090b336c0f170a6e5dcab196125d Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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.
---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index fdd4feb59..2df231f26 100644
--- a/CHANGES
+++ b/CHANGES
@@ -39,6 +39,9 @@ Tactics
   still be used if you really want to ignore universe constraints.
 
 - Tactics and tactic notations now understand the `deprecated` attribute.
+- The `fourier` tactic has been removed. Please now use `lra` instead. You
+  may need to add `Require Import Lra` to your developments. For compatibility,
+  we now define `fourier` as a deprecated alias of `lra`.
 
 Tools
 
-- 
cgit v1.2.3