From a4d496b2424ef991dfdd066e8138c321f62fd017 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 13 Apr 2018 21:12:48 +0200
Subject: Making tactic-in-term aware of "Set Ltac Debug".

---
 CHANGES | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 234d6c0dbf..ed46150211 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,9 +14,9 @@ Vernacular Commands
 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.
+- Option "Ltac Debug" now applies also to terms built using Ltac functions.
 
 Changes from 8.8+beta1 to 8.8.0
 ===============================
-- 
cgit v1.2.3