From d3a51ac24244f586dfeff1a93b68cb084370534e Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 11 Jan 2021 14:47:13 -0800
Subject: Remove the omega tactic and related options

---
 Makefile.dev | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'Makefile.dev')

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:
-- 
cgit v1.2.3