From e17ee7629006dd119393727a3203bc6e602d5473 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 24 Dec 2019 13:23:14 +0100
Subject: Deprecate the "omega with *" syntax.

Changes to the test-suite were backported from PR #11288.
---
 plugins/omega/g_omega.mlg | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/omega/g_omega.mlg b/plugins/omega/g_omega.mlg
index 84964a7bd2..a464aa7287 100644
--- a/plugins/omega/g_omega.mlg
+++ b/plugins/omega/g_omega.mlg
@@ -45,13 +45,16 @@ let omega_tactic l =
     (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 [] }
 END
 
-TACTIC EXTEND omega'
+TACTIC EXTEND omega' DEPRECATED { omega_with_deprecation }
 | [ "omega" "with" ne_ident_list(l) ] ->
     { omega_tactic (List.map Names.Id.to_string l) }
 | [ "omega" "with" "*" ] ->
-- 
cgit v1.2.3