aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES2
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,