diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-18 17:21:01 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-18 17:21:01 +0200 |
| commit | 8271b23dd0a26bba79c7d6dadd92d2329945675c (patch) | |
| tree | 6d6b4faeda0fc272c1faaa7912406097ef055caa /plugins/fourier/g_fourier.mlg | |
| parent | e5e3725fab9daa810a4c8a383886f1c5dc980e85 (diff) | |
| parent | 8c43e795c772090b336c0f170a6e5dcab196125d (diff) | |
Merge PR #7897: Remove fourier plugin
Diffstat (limited to 'plugins/fourier/g_fourier.mlg')
| -rw-r--r-- | plugins/fourier/g_fourier.mlg | 22 |
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 |