aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/fourier/Fourier.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/fourier/Fourier.v')
-rw-r--r--plugins/fourier/Fourier.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
index 1d7ee93ea..a96254713 100644
--- a/plugins/fourier/Fourier.v
+++ b/plugins/fourier/Fourier.v
@@ -13,6 +13,6 @@ Require Export DiscrR.
Require Export Fourier_util.
Declare ML Module "fourier_plugin".
-Ltac fourier := abstract (fourierz; field; discrR).
+Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR).
Ltac fourier_eq := apply Rge_antisym; fourier.