From 27ea35bafdf0aefe1dcf49dfed1a18c3f158efa5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 28 Apr 2007 13:56:03 +0000
Subject: Ajout de la possibilité de faire référence dans certains cas à un nom
 par sa notation (p.ex. pour unfold ou pour lazy delta). Ex: Goal 3+4 = 7.
 unfold "+".

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 48a3123668..1c13955429 100644
--- a/CHANGES
+++ b/CHANGES
@@ -39,6 +39,7 @@ Tactics
   expressions with explicit occurrences of match or fix.
 - Better heuristic of lemma unfolding for apply/eapply.
 - New tactics "eapply in", "erewrite", "erewrite in".
+- Unfoldable references can be given by notation rather than by name in unfold.
 
 Changes from V8.1gamma to V8.1
 ==============================
-- 
cgit v1.2.3