diff options
| -rw-r--r-- | doc/changelog/04-tactics/11288-omega+depr.rst | 6 | ||||
| -rw-r--r-- | plugins/omega/g_omega.mlg | 36 |
2 files changed, 7 insertions, 35 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/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg index a464aa7287..7c653b223e 100644 --- a/plugins/omega/g_omega.mlg +++ b/plugins/omega/g_omega.mlg @@ -21,43 +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) - -let omega_with_deprecation = - Deprecation.make ~since:"8.11.0" ~note:"Use lia instead." () } TACTIC EXTEND omega -| [ "omega" ] -> { omega_tactic [] } +| [ "omega" ] -> { Coq_omega.omega_solver } END - -TACTIC EXTEND omega' DEPRECATED { omega_with_deprecation } -| [ "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 - |