Remove romega

CHANGES

@@ -8,6 +8,10 @@ Plugins
   externally, the Coq development team can provide assistance for extracting
   the plugin and setting up a new repository.
 
+Tactics
+
+- Removed the deprecated `romega` tactics.
+
 Changes from 8.8.2 to 8.9+beta1
 ===============================
 

META.coq.in

@@ -301,18 +301,6 @@ package "plugins" (
     archive(native)  = "omega_plugin.cmx"
   )
 
-  package "romega" (
-
-    description = "Coq romega plugin"
-    version     = "8.10"
-
-    requires    = "coq.plugins.omega"
-    directory   = "romega"
-
-    archive(byte)    = "romega_plugin.cmo"
-    archive(native)  = "romega_plugin.cmx"
-  )
-
   package "micromega" (
 
     description = "Coq micromega plugin"

Makefile.common

@@ -95,7 +95,7 @@ CORESRCDIRS:=\
   tactics 	vernac		stm		toplevel
 
 PLUGINDIRS:=\
-  omega		romega 		micromega \
+  omega		micromega \
   setoid_ring 	extraction \
   cc 		funind 		firstorder 	derive \
   rtauto 	nsatz           syntax          btauto \
@@ -129,7 +129,6 @@ GRAMMARCMA:=grammar/grammar.cma
 ###########################################################################
 
 OMEGACMO:=plugins/omega/omega_plugin.cmo
-ROMEGACMO:=plugins/romega/romega_plugin.cmo
 MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo
 RINGCMO:=plugins/setoid_ring/newring_plugin.cmo
 NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo
@@ -150,7 +149,7 @@ LTACCMO:=plugins/ltac/ltac_plugin.cmo plugins/ltac/tauto_plugin.cmo
 SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo
 SSRCMO:=plugins/ssr/ssreflect_plugin.cmo
 
-PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
+PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(MICROMEGACMO) \
         $(RINGCMO) \
         $(EXTRACTIONCMO) \
         $(CCCMO)  $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \

Makefile.dev

@@ -169,7 +169,6 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \
 ################
 
 OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO))
-ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO))
 MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO))
 RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO))
 NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO))
@@ -181,7 +180,7 @@ CCVO:=
 DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO))
 LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO))
 
-omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
+omega: $(OMEGAVO) $(OMEGACMO)
 micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
 setoid_ring: $(RINGVO) $(RINGCMO)
 nsatz: $(NSATZVO) $(NSATZCMO)

dev/ocamldebug-coq.run

@@ -37,7 +37,7 @@ if [ -z "$GUESS_CHECKER" ]; then
         -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
         -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
         -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
-        -I $COQTOP/plugins/ring       -I $COQTOP/plugins/romega \
+        -I $COQTOP/plugins/ring \
 	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
         -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
         -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \

dev/v8-syntax/syntax-v8.tex

@@ -765,8 +765,6 @@ \subsection{Other tactics}
 %% plugins/ring
 \nlsep \TERM{quote}~\NT{ident}~\OPTGR{\KWD{[}~\PLUS{\NT{ident}}~\KWD{]}}
 \nlsep \TERM{ring}~\STAR{\tacconstr}
-%% plugins/romega
-\nlsep \TERM{romega}
 \SEPDEF
 \DEFNT{orient}
        \KWD{$\rightarrow$}~\mid~\KWD{$\leftarrow$}

doc/sphinx/addendum/micromega.rst

@@ -112,20 +112,19 @@ and checked to be :math:`-1`.
 .. tacn:: lia
    :name: lia
 
-This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega`
-tactics. Roughly speaking, the deductive power of lia is the combined deductive
-power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear
-goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following
-so-called *omega nightmare* :cite:`TheOmegaPaper`.
+   This tactic offers an alternative to the :tacn:`omega` tactic. Roughly
+   speaking, the deductive power of lia is the combined deductive power of
+   :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals
+   that :tacn:`omega` does not solve, such as the following so-called *omega
+   nightmare* :cite:`TheOmegaPaper`.
 
 .. coqtop:: in
 
    Goal forall x y,
      27 <= 11 * x + 13 * y <= 45 ->
      -10 <= 7 * x - 9 * y <= 4 -> False.
 
-The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and
-:tacn:`romega` is under evaluation.
+The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation.
 
 High level view of `lia`
 ~~~~~~~~~~~~~~~~~~~~~~~~

doc/sphinx/addendum/omega.rst

@@ -23,13 +23,6 @@ Description of ``omega``
    If the tactic cannot solve the goal, it fails with an error message.
    In any case, the computation eventually stops.
 
-.. tacv:: romega
-   :name: romega
-
-   .. deprecated:: 8.9
-
-      Use :tacn:`lia` instead.
-
 Arithmetical goals recognized by ``omega``
 ------------------------------------------
 

plugins/btauto/Reflect.v

@@ -1,4 +1,4 @@
-Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega.
+Require Import Bool DecidableClass Algebra Ring PArith Omega.
 
 Section Bool.