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

diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 8504a06f4..d68e3fd22 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -9,7 +9,7 @@
 (* Decidable setoid equality theory.
  *
  * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
  *              91405 Orsay, France *)
 
 (* $Id$ *)
@@ -75,18 +75,18 @@ Require Import Coq.Arith.Arith.
 (** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
 
 Program Instance eq_setoid A : Setoid A | 10 :=
-  equiv := eq ; setoid_equiv := eq_equivalence.
+  { equiv := eq ; setoid_equiv := eq_equivalence }.
 
 Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) :=
-  equiv_dec := eq_nat_dec.
+  eq_nat_dec.
 
 Require Import Coq.Bool.Bool.
 
 Program Instance bool_eqdec : EqDec (eq_setoid bool) :=
-  equiv_dec := bool_dec.
+  bool_dec.
 
 Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
-  equiv_dec x y := in_left.
+  λ x y, in_left.
 
   Next Obligation.
   Proof.
@@ -95,7 +95,7 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
   Qed.
 
 Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) :=
-  equiv_dec x y := 
+  λ x y,
     let '(x1, x2) := x in 
     let '(y1, y2) := y in 
     if x1 == y1 then 
@@ -108,7 +108,7 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : Eq
 (** Objects of function spaces with countable domains like bool have decidable equality. *)
 
 Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) :=
-  equiv_dec f g := 
+  λ f g,
     if f true == g true then
       if f false == g false then in_left
       else in_right