Merge PR #677: Trunk+abstracting injection flags

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 640ab4aa50..7a326c589a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,8 @@ Tactics
   such as "x := 5 : Z" (see BZ#148). This could be disabled via
   Unset Omega UseLocalDefs.
 - The tactic "romega" is also aware now of the bodies of context variables.
+- Tactic "decide equality" now able to manage constructors which
+  contain proofs.
 
 Changes from 8.7+beta2 to 8.7.0
 ===============================