From 6f139b30496d263504eee9574a9e54a919ab71d2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 11 Jul 2006 14:02:49 +0000
Subject: MAJ

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index de640f102f..b134073bf3 100644
--- a/CHANGES
+++ b/CHANGES
@@ -34,7 +34,8 @@ Ltac and tactic syntactic extensions
 - New semantics for "match t with": if a clause returns a
   tactic, it is now applied to the current goal. If it fails, the next
   clause or next matching subterm is tried (i.e. it behaves as "match
-  goal with" does) (doc TODO-HH).
+  goal with" does). The keyword "lazymatch" can be used to delay the 
+  evaluation of tactics occurring in matching clauses.
 - Hint base names can be parametric in auto and trivial.
 - Occurrence values can be parametric in unfold, pattern, etc.
 - Added entry constr_may_eval for tactic extensions.
-- 
cgit v1.2.3