aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/fourier/Fourier.v
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/fourier/Fourier.v')
-rw-r--r--contrib/fourier/Fourier.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/fourier/Fourier.v b/contrib/fourier/Fourier.v
index a97869b32..ac1592bee 100644
--- a/contrib/fourier/Fourier.v
+++ b/contrib/fourier/Fourier.v
@@ -17,7 +17,7 @@ Declare ML Module "fourierR".
Declare ML Module "field".
Require Export Fourier_util.
-Require Export Field.
+Require Export LegacyField.
Require Export DiscrR.
Ltac fourier := abstract (fourierz; field; discrR).