Deprecate romega in favor of lia.

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 5d1c9a9c2d..45f8622d11 100644
--- a/CHANGES
+++ b/CHANGES
@@ -48,6 +48,8 @@ Tactics
   may need to add `Require Import Lra` to your developments. For compatibility,
   we now define `fourier` as a deprecated alias of `lra`.
 
+- The `romega` tactics have been deprecated; please use `lia` instead.
+
 Focusing
 
 - Focusing bracket `{` now supports named goal selectors,