From 2d3335cbd6a34f8d5d3c7444a68dba7399d817a7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Sep 2005 21:08:52 +0000
Subject: Declare Implicit Tactic

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7365 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGES b/CHANGES
index dcd395e68a..7b8b5b5970 100644
--- a/CHANGES
+++ b/CHANGES
@@ -47,6 +47,8 @@ Tactics
 - Fixed a "fold" bug (non critical and possible source of incompatibilities).
 - Added classical_left and classical_right which transforms |- A \/ B into 
   ~B |- A and ~A |- B respectively.
+- Added command "Declare Implicit Tactic" to set up a default tactic to be
+  used to solve unresolved subterms of term arguments of tactics.
 
 Modules
 
-- 
cgit v1.2.3