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, 3 insertions, 3 deletions

diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 78616a9a4..ae03e28e5 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -56,7 +56,7 @@ Existing Instance setoid_trans.
 (*   equiv := eq ; setoid_equiv := eq_equivalence. *)
 
 Program Instance iff_setoid : Setoid Prop := 
-  equiv := iff ; setoid_equiv := iff_equivalence.
+  { equiv := iff ; setoid_equiv := iff_equivalence }.
 
 (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
 
@@ -120,10 +120,10 @@ Ltac setoidify := repeat setoidify_tac.
 (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
 
 Program Instance setoid_morphism `(sa : Setoid A) : Morphism (equiv ++> equiv ++> iff) equiv :=
-  respect := respect.
+  respect.
 
 Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Morphism (equiv ++> iff) (equiv x) :=
-  respect := respect.
+  respect.
 
 Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.