Remove the omega tactic and related options

2 files changed, 0 insertions, 211 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 5d471c695c..d718454364 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -159,7 +159,6 @@ and checked to be :math:`-1`.
    This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes.
    :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic.
 
-
 High level view of `lia`
 ~~~~~~~~~~~~~~~~~~~~~~~~
 
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
deleted file mode 100644
index 86bb0502c6..0000000000
--- a/doc/sphinx/addendum/omega.rst
+++ /dev/null
@@ -1,210 +0,0 @@
-.. _omega_chapter:
-
-Omega: a (deprecated) solver for arithmetic
-=====================================================================
-
-:Author: Pierre Crégut
-
-.. warning::
-
-   The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia`
-   tactic.  The goal is to consolidate the arithmetic solving
-   capabilities of Coq into a single engine; moreover, :tacn:`lia` is
-   in general more powerful than :tacn:`omega` (it is a complete
-   Presburger arithmetic solver while :tacn:`omega` was known to be
-   incomplete).
-
-   It is recommended to switch from :tacn:`omega` to :tacn:`lia` in existing
-   projects.  We also ask that you report (in our `bug tracker
-   <https://github.com/coq/coq/issues>`_) any issue you encounter, especially
-   if the issue was not present in :tacn:`omega`.  If no new issues are
-   reported, :tacn:`omega` will be removed soon.
-
-   Note that replacing :tacn:`omega` with :tacn:`lia` can break
-   non-robust proof scripts which rely on incompleteness bugs of
-   :tacn:`omega` (e.g. using the pattern :g:`; try omega`).
-
-Description of ``omega``
-------------------------
-
-.. tacn:: omega
-
-   .. deprecated:: 8.12
-
-      Use :tacn:`lia` instead.
-
-   :tacn:`omega` is a tactic for solving goals in Presburger arithmetic,
-   i.e. for proving formulas made of equations and inequalities over the
-   type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers.
-   Formulas on ``nat`` are automatically injected into ``Z``. The procedure
-   may use any hypothesis of the current proof session to solve the goal.
-
-   Multiplication is handled by :tacn:`omega` but only goals where at
-   least one of the two multiplicands of products is a constant are
-   solvable. This is the restriction meant by "Presburger arithmetic".
-
-   If the tactic cannot solve the goal, it fails with an error message.
-   In any case, the computation eventually stops.
-
-Arithmetical goals recognized by ``omega``
-------------------------------------------
-
-:tacn:`omega` applies only to quantifier-free formulas built from the connectives::
-
-   /\  \/  ~  ->
-
-on atomic formulas. Atomic formulas are built from the predicates::
-
-   =  <  <=  >  >=
-
-on ``nat`` or ``Z``. In expressions of type ``nat``, :tacn:`omega` recognizes::
-
-   +  -  *  S  O  pred
-
-and in expressions of type ``Z``, :tacn:`omega` recognizes numeral constants and::
-
-   +  -  *  Z.succ Z.pred
-
-All expressions of type ``nat`` or ``Z`` not built on these
-operators are considered abstractly as if they
-were arbitrary variables of type ``nat`` or ``Z``.
-
-Messages from ``omega``
------------------------
-
-When :tacn:`omega` does not solve the goal, one of the following errors
-is generated:
-
-.. exn:: omega can't solve this system.
-
-  This may happen if your goal is not quantifier-free (if it is
-  universally quantified, try :tacn:`intros` first; if it contains
-  existentials quantifiers too, :tacn:`omega` is not strong enough to solve your
-  goal). This may happen also if your goal contains arithmetical
-  operators not recognized by :tacn:`omega`. Finally, your goal may be simply
-  not true!
-
-.. exn:: omega: Not a quantifier-free goal.
-
-  If your goal is universally quantified, you should first apply
-  :tacn:`intro` as many times as needed.
-
-.. exn:: omega: Unrecognized predicate or connective: @ident.
-   :undocumented:
-
-.. exn:: omega: Unrecognized atomic proposition: ...
-   :undocumented:
-
-.. exn:: omega: Can't solve a goal with proposition variables.
-   :undocumented:
-
-.. exn:: omega: Unrecognized proposition.
-   :undocumented:
-
-.. exn:: omega: Can't solve a goal with non-linear products.
-   :undocumented:
-
-.. exn:: omega: Can't solve a goal with equality on type ...
-   :undocumented:
-
-
-Using ``omega``
----------------
-
-The ``omega`` tactic does not belong to the core system. It should be
-loaded by
-
-.. coqtop:: in
-
-   Require Import Omega.
-
-.. example::
-
-  .. coqtop:: all warn
-
-     Require Import Omega.
-
-     Open Scope Z_scope.
-
-     Goal forall m n:Z, 1 + 2 * m <> 2 * n.
-     intros; omega.
-     Abort.
-
-     Goal forall z:Z, z > 0 -> 2 * z + 1 > z.
-     intro; omega.
-     Abort.
-
-
-Options
--------
-
-.. flag:: Stable Omega
-
-   .. deprecated:: 8.5
-
-   This deprecated flag (on by default) is for compatibility with Coq pre 8.5. It
-   resets internal name counters to make executions of :tacn:`omega` independent.
-
-.. flag:: Omega UseLocalDefs
-
-   This flag (on by default) allows :tacn:`omega` to use the :term:`bodies <body>` of local
-   variables.
-
-.. flag:: Omega System
-
-   This flag (off by default) activate the printing of debug information
-
-.. flag:: Omega Action
-
-   This flag (off by default) activate the printing of debug information
-
-Technical data
---------------
-
-Overview of the tactic
-~~~~~~~~~~~~~~~~~~~~~~
-
- * The goal is negated twice and the first negation is introduced as a hypothesis.
- * Hypotheses are decomposed in simple equations or inequalities. Multiple
-   goals may result from this phase.
- * Equations and inequalities over ``nat`` are translated over
-   ``Z``, multiple goals may result from the translation of subtraction.
- * Equations and inequalities are normalized.
- * Goals are solved by the OMEGA decision procedure.
- * The script of the solution is replayed.
-
-Overview of the OMEGA decision procedure
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
-The OMEGA decision procedure involved in the :tacn:`omega` tactic uses
-a small subset of the decision procedure presented in :cite:`TheOmegaPaper`
-Here is an overview, refer to the original paper for more information.
-
- * Equations and inequalities are normalized by division by the GCD of their
-   coefficients.
- * Equations are eliminated, using the Banerjee test to get a coefficient
-   equal to one.
- * Note that each inequality cuts the Euclidean space in half.
- * Inequalities are solved by projecting on the hyperspace
-   defined by cancelling one of the variables. They are partitioned
-   according to the sign of the coefficient of the eliminated
-   variable. Pairs of inequalities from different classes define a
-   new edge in the projection.
- * Redundant inequalities are eliminated or merged in new
-   equations that can be eliminated by the Banerjee test.
- * The last two steps are iterated until a contradiction is reached
-   (success) or there is no more variable to eliminate (failure).
-
-It may happen that there is a real solution and no integer one. The last
-steps of the Omega procedure are not implemented, so the
-decision procedure is only partial.
-
-Bugs
-----
-
- * The simplification procedure is very dumb and this results in
-   many redundant cases to explore.
-
- * Much too slow.
-
- * Certainly other bugs! You can report them to https://coq.inria.fr/bugs/.