1 files changed, 4 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index a9fbfe29d0..cda16d3804 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,10 @@ Tactics
 - Flag "Bracketing Last Introduction Pattern" is now on by default.
 - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract
   tactical w.r.t. variables appearing in the body of the proof.
+- Serious bugs are fixed in tactic "double induction" (source of
+  incompatibilities as soon as the inductive types have dependencies in
+  the type of their constructors; "double induction" remains however
+  deprecated).
 
 Program