From f44ddd58ffb19ad08389580c76de2130e7cd1197 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 19 Nov 2010 10:20:05 +0000
Subject: CHANGES: small re-sync with the one of branch v8.3

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

diff --git a/CHANGES b/CHANGES
index beb9ebab20..2d3ac54268 100644
--- a/CHANGES
+++ b/CHANGES
@@ -20,7 +20,8 @@ Rewriting tactics
   proofs that are dependent (use "simple subst" for preserving compatibility).
 - Added support for Leibniz-rewriting of dependent hypotheses.
 - Renamed "Morphism" into "Proper" and "respect" into "proper_prf"
-  (possible source of incompatibility).
+  (possible source of incompatibility). A partial fix is to define
+  "Notation Morphism R f := (Proper (R%signature) f)."
 - New tactic variants "rewrite* by" and "autorewrite*" that rewrite
   respectively the first and all matches whose side-conditions are
   solved.
-- 
cgit v1.2.3