Merge PR #11288: [omega] Remove non-documented "omega with *"

Reviewed-by: Zimmi48
Ack-by: maximedenes

5 files changed, 34 insertions, 53 deletions

diff --git a/doc/changelog/04-tactics/11288-omega+depr.rst b/doc/changelog/04-tactics/11288-omega+depr.rst
new file mode 100644
index 0000000000..2832e6db61
--- /dev/null
+++ b/doc/changelog/04-tactics/11288-omega+depr.rst
@@ -0,0 +1,6 @@
+- **Removed:**
+  The undocumented ``omega with`` tactic variant has been removed,
+  using ``lia`` is the recommended replacement, tho the old semantics
+  of ``omega with *`` can be recovered with ``zify; omega``
+  (`#11288 <https://github.com/coq/coq/pull/11288>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/doc/changelog/04-tactics/11337-omega-with-depr.rst b/doc/changelog/04-tactics/11337-omega-with-depr.rst
new file mode 100644
index 0000000000..25e929e030
--- /dev/null
+++ b/doc/changelog/04-tactics/11337-omega-with-depr.rst
@@ -0,0 +1,6 @@
+- **Deprecated:**
+  The undocumented ``omega with`` tactic variant has been deprecated,
+  using ``lia`` is the recommended replacement, tho the old semantics
+  of ``omega with *`` can be recovered with ``zify; omega``
+  (`#11337 <https://github.com/coq/coq/pull/11337>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg
index 84964a7bd2..7c653b223e 100644
--- a/plugins/omega/g_omega.mlg
+++ b/plugins/omega/g_omega.mlg
@@ -21,40 +21,9 @@ DECLARE PLUGIN "omega_plugin"
 {
 
 open Ltac_plugin
-open Names
-open Coq_omega
-open Stdarg
-
-let eval_tactic name =
-  let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in
-  let kn = KerName.make (ModPath.MPfile dp) (Label.make name) in
-  let tac = Tacenv.interp_ltac kn in
-  Tacinterp.eval_tactic tac
-
-let omega_tactic l =
-  let tacs = List.map
-    (function
-       | "nat" -> eval_tactic "zify_nat"
-       | "positive" -> eval_tactic "zify_positive"
-       | "N" -> eval_tactic "zify_N"
-       | "Z" -> eval_tactic "zify_op"
-       | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s)))
-    (Util.List.sort_uniquize String.compare l)
-  in
-  Tacticals.New.tclTHEN
-    (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs))
-    (omega_solver)
 
 }
 
 TACTIC EXTEND omega
-|  [ "omega" ] -> { omega_tactic [] }
+|  [ "omega" ] -> { Coq_omega.omega_solver }
 END
-
-TACTIC EXTEND omega'
-| [ "omega" "with" ne_ident_list(l) ] ->
-    { omega_tactic (List.map Names.Id.to_string l) }
-| [ "omega" "with" "*" ] ->
-  { Tacticals.New.tclTHEN (eval_tactic "zify") (omega_tactic []) }
-END
-
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index 470e4f0580..5e0f90d59b 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -90,5 +90,5 @@ Qed.
 (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
 Lemma lem10 : forall n m:nat, le n (plus n (mult n m)).
 Proof.
-intros; omega with *.
+intros; zify; omega.
 Qed.
diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v
index 17531064cc..0223255067 100644
--- a/test-suite/success/OmegaPre.v
+++ b/test-suite/success/OmegaPre.v
@@ -16,112 +16,112 @@ Open Scope Z_scope.
 
 Goal forall a:Z, Z.max a a = a.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall a b:Z, Z.max a b = Z.max b a.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
 intros.
 zify.
-intuition; subst; omega. (* pure multiplication: omega alone can't do it *)
+intuition; subst; zify; omega. (* pure multiplication: zify; omega alone can't do it *)
 Qed.
 
 Goal forall a:Z, Z.abs a = a -> a >= 0.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 (* zify_nat *)
 
 Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
 intros.
-omega with *.
+zify; omega.
 Qed.
 (* 2000 instead of 200: works, but quite slow *)
 
 Goal forall m: nat, (m*m>=0)%nat.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 (* zify_positive *)
 
 Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m: positive, (m*m>=1)%positive.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 (* zify_N *)
 
 Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m:N, (m<1)%N -> (m=0)%N.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m:N, (m*m>=0)%N.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 (* mix of datatypes *)
 
 Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
 intros.
-omega with *.
+zify; omega.
 Qed.