Merge PR #6555: Use let-in aware prod_applist_assum in dtauto and firstorder.

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 289b7d5d2d..c9197fb36e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -40,6 +40,8 @@ Tactics
 - Added tactic optimize_heap, analogous to the Vernacular Optimize
   Heap, which performs a major garbage collection and heap compaction
   in the OCaml run-time system.
+- The tactics "dtauto", "dintuition", "firstorder" now handle inductive types
+  with let bindings in the parameters.
 
 Focusing