Last changes in type class syntax:

- curly braces mandatory for record class instances
- no mention of the unique method for definitional class instances
Turning a record or definition into a class is mostly a 
matter of changing the keywords to 'Class' and 'Instance' now.
Documentation reflects these changes, and was checked once more 
along with setoid_rewrite's and Program's.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11797 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 4 deletions

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index b9256bdbc..659289f88 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -71,10 +71,10 @@ Hint Extern 4 => solve_relation : relations.
 (** We can already dualize all these properties. *)
 
 Program Instance flip_Reflexive `(Reflexive A R) : Reflexive (flip R) :=
-  reflexivity := reflexivity (R:=R).
+  reflexivity (R:=R).
 
 Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
-  irreflexivity := irreflexivity (R:=R).
+  irreflexivity (R:=R).
 
 Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R).
 
@@ -168,8 +168,8 @@ Class Equivalence {A} (R : relation A) : Prop := {
 (** An Equivalence is a PER plus reflexivity. *)
 
 Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
-  PER_Symmetric := Equivalence_Symmetric ;
-  PER_Transitive := Equivalence_Transitive.
+  { PER_Symmetric := Equivalence_Symmetric ;
+    PER_Transitive := Equivalence_Transitive }.
 
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)