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.v3
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
index a1113d2d0..1e944a452 100644
--- a/plugins/fourier/Fourier.v
+++ b/plugins/fourier/Fourier.v
@@ -8,8 +8,7 @@
(* "Fourier's method to solve linear inequations/equations systems.".*)
-Require Export LegacyRing.
-Require Export LegacyField.
+Require Export Field.
Require Export DiscrR.
Require Export Fourier_util.
Declare ML Module "fourier_plugin".