diff options
Diffstat (limited to 'contrib/fourier/Fourier.v')
| -rw-r--r-- | contrib/fourier/Fourier.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/contrib/fourier/Fourier.v b/contrib/fourier/Fourier.v index 67d734281d..32c61b6d2d 100644 --- a/contrib/fourier/Fourier.v +++ b/contrib/fourier/Fourier.v @@ -14,14 +14,20 @@ Declare ML Module "quote". Declare ML Module "ring". Declare ML Module "fourier". Declare ML Module "fourierR". +Declare ML Module "field". Require Export Fourier_util. +Require Export Field. +Require Export DiscrR. Grammar tactic simple_tactic:ast:= fourier - ["Fourier" constrarg_list($arg)] -> + ["FourierZ" constrarg_list($arg)] -> [(Fourier ($LIST $arg))]. +Tactic Definition Fourier := + Abstract (FourierZ;Field;DiscrR). + Tactic Definition FourierEq := Apply Rge_ge_eq ; Fourier. |