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. --- theories/Reals/Reals.v | 1 + 1 file changed, 1 insertion(+) (limited to 'theories/Reals/Reals.v') diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index b249b519f..3ef368bb4 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -30,3 +30,4 @@ Require Export SeqSeries. Require Export Rtrigo. Require Export Ranalysis. Require Export Integration. +Require Import Fourier. -- cgit v1.2.3