Merge PR #7229: Deprecate implicit tactic solving.

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 5b5885487a..e8718bbab7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -23,6 +23,8 @@ Tactics
 
 - Option "Ltac Debug" now applies also to terms built using Ltac functions.
 
+- Deprecated the Implicit Tactic family of commands.
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from