From ddc25ec6150005e949442d422549fbc213d8f4af Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Thu, 6 Sep 2018 17:49:28 +0200
Subject: Deprecate romega in favor of lia.

---
 plugins/romega/g_romega.mlg | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'plugins/romega')

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"] }
-- 
cgit v1.2.3