aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
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 dc40413078..a21e974ed5 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -102,7 +102,7 @@ CORESRCDIRS:=\
tactics vernac stm sysinit toplevel
PLUGINDIRS:=\
- omega micromega \
+ micromega \
ring extraction \
cc funind firstorder derive \
rtauto nsatz syntax btauto \
@@ -138,7 +138,6 @@ CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/l
# plugins object files
###########################################################################
-OMEGACMO:=plugins/omega/omega_plugin.cmo
MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
RINGCMO:=plugins/ring/ring_plugin.cmo
NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
@@ -159,7 +158,7 @@ SSRSEARCHCMO=plugins/ssrsearch/ssrsearch_plugin.cmo
LTAC2CMO:=user-contrib/Ltac2/ltac2_plugin.cmo
ZIFYCMO:=plugins/micromega/zify_plugin.cmo
-PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \
+PLUGINSCMO:=$(LTACCMO) $(MICROMEGACMO) \
$(RINGCMO) \
$(EXTRACTIONCMO) \
$(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \