aboutsummaryrefslogtreecommitdiff
path: root/Makefile.common
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-04-06 14:55:06 +0000
committerGitHub2021-04-06 14:55:06 +0000
commit2360e5ba31c350f25d49fc71736282bfad9975ed (patch)
tree6c3204f2ef382d452ad8684fd46e5e10a81be5c4 /Makefile.common
parentdc565f2898145536cc6d3cf4346b6a60726bb8a9 (diff)
parentd3a51ac24244f586dfeff1a93b68cb084370534e (diff)
Merge PR #13741: Remove omega tactic (deprecated in 8.12)
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: silene Ack-by: SkySkimmer Ack-by: olaure01
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) \