From ec850ff623801e514b3ed0a42beb6f7984992520 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 7 Mar 2008 16:32:12 +0000
Subject: Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As
 part of the fix I added an optional "by" annotation for rewrite to solve said
 conditions in the same tactic call. Most of the theories have been updated,
 only FSets is missing, Pierre will take care of it.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index e93eb275ca..3bba84fc75 100644
--- a/CHANGES
+++ b/CHANGES
@@ -10,7 +10,7 @@ Language
 - New experimental typeclass system giving ad-hoc polymorphism and 
   overloading based on dependent records and implicit arguments.
 - New syntax "let| pat := b in c" for let-binding using irrefutable patterns.
-- New syntax "forall `A`, T" for specifying maximally inserted implicit 
+- New syntax "forall {A}, T" for specifying maximally inserted implicit 
   arguments in terms.
 
 Commands
@@ -139,9 +139,9 @@ Type Classes
 - New theories directory "theories/Classes" for standard typeclasses 
   declarations. Module Classes.Relations is a typeclass port of 
   Relation_Definitions.
-- New experimental "setoid" rewriting tactic "clrewrite" based on typeclasses.
-  Classes.Morphisms declares standard morphisms, Classes.SetoidClasses declares 
-  the new Setoid typeclass.  
+- New experimental "setoid" rewriting tactic based on typeclasses.
+  Classes.Morphisms declares standard morphisms, Classes.Equivalence declares 
+  the new Setoid typeclass and some derived tactics.
   
 Program
 
-- 
cgit v1.2.3