From e85d10cc40e968ea3d16ca32a58ac4b3caf2b100 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 5 Oct 2006 13:26:31 +0000
Subject: avertissement a propos du commit 9211 dans CHANGES

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

diff --git a/CHANGES b/CHANGES
index 1cce399c3d..577a828f3d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,8 +12,10 @@ Changes from V8.1beta to V8.1
   infer the predicate in "(exist _ 0 (refl_equal 0) : {n:nat | n=0 })")
 - Support for "where" clause in cofixpoint definitions
 - Support for argument lists of arbitrary length in Tactic Notation
-- [rewrite ... in H] now fails if [H] is used either in an hypohesis
-  or in the goal
+- [rewrite ... in H] now fails if [H] is used either in an hypothesis
+  or in the goal. 
+- The semantics of [rewrite ... in *] has been slightly modified (see doc). 
+
 
 Changes from V8.0 to V8.1beta
 =============================
-- 
cgit v1.2.3