From 88d15de0cc467368dc71851e995d82093f9692ca Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 11 Jan 2006 09:04:44 +0000
Subject: Ajout paramétricité du nom de la base de hint dans auto et trivial
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/CHANGES b/CHANGES
index 94303fad3..cf0d007ea 100644
--- a/CHANGES
+++ b/CHANGES
@@ -32,6 +32,7 @@ Ltac
   goal with").
 - New modifier "lazy" (TODO) for "match t with" and "match goal with" telling
   to delay the evaluation of tactic expression.
+- Hint base name can be parametric in auto and trivial.
 
 Tactics
 
-- 
cgit v1.2.3