diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-07 16:32:12 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-07 16:32:12 +0000 |
| commit | ec850ff623801e514b3ed0a42beb6f7984992520 (patch) | |
| tree | 6a03dd3d0545b927326f28e7d8da08a850cead5f /CHANGES | |
| parent | 905c47d6a07cc69b9e7aa0b9d73caeacf2b1d2be (diff) | |
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
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -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 |