aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/fourier/g_fourier.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/fourier/g_fourier.ml4')
-rw-r--r--contrib/fourier/g_fourier.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/fourier/g_fourier.ml4 b/contrib/fourier/g_fourier.ml4
index 620cabe80..b952851fa 100644
--- a/contrib/fourier/g_fourier.ml4
+++ b/contrib/fourier/g_fourier.ml4
@@ -12,6 +12,6 @@
open FourierR
-TACTIC EXTEND Fourier
- [ "FourierZ" (* constr_list(l) *) ] -> [ fourier (* l *) ]
+TACTIC EXTEND fourier
+ [ "fourierz" ] -> [ fourier ]
END