aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/fourier/g_fourier.mlg
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/fourier/g_fourier.mlg')
-rw-r--r--plugins/fourier/g_fourier.mlg22
1 files changed, 0 insertions, 22 deletions
diff --git a/plugins/fourier/g_fourier.mlg b/plugins/fourier/g_fourier.mlg
deleted file mode 100644
index 703e29f96..000000000
--- a/plugins/fourier/g_fourier.mlg
+++ /dev/null
@@ -1,22 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-{
-
-open Ltac_plugin
-open FourierR
-
-}
-
-DECLARE PLUGIN "fourier_plugin"
-
-TACTIC EXTEND fourier
-| [ "fourierz" ] -> { fourier () }
-END