Merge PR #6407: Fix #6404 - Print tactics called by ML tactics

1 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 37d9d36808..3994caef67 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,9 @@ Tactic language
 
 - Support for fix/cofix added in Ltac "match" and "lazymatch".
 
+- Ltac backtraces now contain include trace information about tactics
+  called by OCaml-defined tactics.
+
 Changes from 8.7.2 to 8.8+beta1
 ===============================