aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-07-18 17:21:01 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2018-07-18 17:21:01 +0200
commit8271b23dd0a26bba79c7d6dadd92d2329945675c (patch)
tree6d6b4faeda0fc272c1faaa7912406097ef055caa /Makefile.common
parente5e3725fab9daa810a4c8a383886f1c5dc980e85 (diff)
parent8c43e795c772090b336c0f170a6e5dcab196125d (diff)
Merge PR #7897: Remove fourier plugin
Diffstat (limited to 'Makefile.common')
-rw-r--r--Makefile.common5
1 files changed, 2 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common
index 727cb1e69..772561bd7 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -96,7 +96,7 @@ CORESRCDIRS:=\
PLUGINDIRS:=\
omega romega micromega quote \
- setoid_ring extraction fourier \
+ setoid_ring extraction \
cc funind firstorder derive \
rtauto nsatz syntax btauto \
ssrmatching ltac ssr
@@ -134,7 +134,6 @@ MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
QUOTECMO:=plugins/quote/quote_plugin.cmo
RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
-FOURIERCMO:=plugins/fourier/fourier_plugin.cmo
EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo
FUNINDCMO:=plugins/funind/recdef_plugin.cmo
FOCMO:=plugins/firstorder/ground_plugin.cmo
@@ -155,7 +154,7 @@ SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
$(QUOTECMO) $(RINGCMO) \
- $(FOURIERCMO) $(EXTRACTIONCMO) \
+ $(EXTRACTIONCMO) \
$(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \
$(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \
$(DERIVECMO) $(SSRMATCHINGCMO) $(SSRCMO)