From b7598d22d98e9ead0516068a9bf6ed37b6d13893 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 23 Oct 2019 10:04:27 +0000
Subject: Deprecate “omega”

---
 plugins/omega/coq_omega.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'plugins')

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 2eef459217..79d6c05e1d 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1899,8 +1899,15 @@ let destructure_goal =
 
 let destructure_goal = destructure_goal
 
+let warn_omega_is_deprecated =
+  let name = "omega-is-deprecated" in
+  let category = "deprecated" in
+  CWarnings.create ~name ~category (fun () ->
+    Pp.str "omega is deprecated since 8.12; use “lia” instead.")
+
 let omega_solver =
   Proofview.tclUNIT () >>= fun () -> (* delay for [check_required_library] *)
+  warn_omega_is_deprecated ();
   Coqlib.check_required_library ["Coq";"omega";"Omega"];
   reset_all ();
   destructure_goal
-- 
cgit v1.2.3