Merge PR #8425: Deprecate romega in favor of lia

1 files changed, 8 insertions, 0 deletions

diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg
index c1ce30027e..ac4f30b1db 100644
--- a/plugins/romega/g_romega.mlg
+++ b/plugins/romega/g_romega.mlg
@@ -41,14 +41,22 @@ let romega_tactic unsafe l =
        (Tactics.intros)
        (total_reflexive_omega_tactic unsafe))
 
+let romega_depr =
+  Vernacinterp.mk_deprecation
+    ~since:(Some "8.9")
+    ~note:(Some "Use lia instead.")
+    ()
+
 }
 
 TACTIC EXTEND romega
+DEPRECATED { romega_depr }
 |  [ "romega" ] -> { romega_tactic false [] }
 |  [ "unsafe_romega" ] -> { romega_tactic true [] }
 END
 
 TACTIC EXTEND romega'
+DEPRECATED { romega_depr }
 | [ "romega" "with" ne_ident_list(l) ] ->
     { romega_tactic false (List.map Names.Id.to_string l) }
 | [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] }