aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dev
diff options
context:
space:
mode:
authorJim Fehrle2021-01-11 14:47:13 -0800
committerJim Fehrle2021-04-02 18:52:59 -0700
commitd3a51ac24244f586dfeff1a93b68cb084370534e (patch)
tree99559dce00d49471fdea5deaff58e0dab481d941 /Makefile.dev
parent012b8a08f142d39b2211fd52c811f830f88f2075 (diff)
Remove the omega tactic and related options
Diffstat (limited to 'Makefile.dev')
-rw-r--r--Makefile.dev4
1 files changed, 1 insertions, 3 deletions
diff --git a/Makefile.dev b/Makefile.dev
index cfb02b6d80..c573fccf95 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -141,7 +141,6 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \
### 4) plugins
################
-OMEGAVO:=$(filter theories/omega/%, $(THEORIESVO))
MICROMEGAVO:=$(filter theories/micromega/%, $(THEORIESVO))
RINGVO:=$(filter theories/setoid_ring/%, $(THEORIESVO))
NSATZVO:=$(filter theories/nsatz/%, $(THEORIESVO))
@@ -153,7 +152,6 @@ CCVO:=
DERIVEVO:=$(filter theories/derive/%, $(THEORIESVO))
LTACVO:=$(filter theories/ltac/%, $(THEORIESVO))
-omega: $(OMEGAVO) $(OMEGACMO)
micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
ring: $(RINGVO) $(RINGCMO)
nsatz: $(NSATZVO) $(NSATZCMO)
@@ -164,7 +162,7 @@ rtauto: $(RTAUTOVO) $(RTAUTOCMO)
btauto: $(BTAUTOVO) $(BTAUTOCMO)
ltac: $(LTACVO) $(LTACCMO)
-.PHONY: omega micromega ring nsatz extraction
+.PHONY: micromega ring nsatz extraction
.PHONY: funind cc rtauto btauto ltac
# For emacs: