From d9a7712b231f92882c2dccdc62d24ea3109abb0e Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 12 Dec 2017 13:52:42 -0500
Subject: Fix #6404 - Print tactics called by ML tactics

---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

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
 ===============================
 
-- 
cgit v1.2.3