1 files changed, 15 insertions, 17 deletions
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index f68a7d3a4b..0a86233166 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -27,12 +27,12 @@ Require Export Coq.Classes.SetoidClass.
 
 Require Import Coq.Logic.Decidable.
 
-Class [ Setoid A R ] => DecidableSetoid :=
+Class [ Setoid A ] => DecidableSetoid :=
   setoid_decidable : forall x y : A, decidable (x == y).
 
 (** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
-Class [ Setoid A R ] => EqDec :=
+Class [ Setoid A ] => EqDec :=
   equiv_dec : forall x y : A, { x == y } + { x =/= y }.
 
 (** We define the [==] overloaded notation for deciding equality. It does not take precedence
@@ -44,15 +44,15 @@ Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70)
 
 Definition swap_sumbool `A B` (x : { A } + { B }) : { B } + { A } :=
   match x with
-    | left H => right _ H 
-    | right H => left _ H 
+    | left H => @right _ _ H 
+    | right H => @left _ _ H 
   end.
 
 Require Import Coq.Program.Program.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec [ EqDec A R ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
+Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x == y } := swap_sumbool (x == y).
 
 (** Overloaded notation for inequality. *)
 
@@ -60,10 +60,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70).
 
 (** Define boolean versions, losing the logical information. *)
 
-Definition equiv_decb [ EqDec A R ] (x y : A) : bool :=
+Definition equiv_decb [ EqDec A ] (x y : A) : bool :=
   if x == y then true else false.
 
-Definition nequiv_decb [ EqDec A R ] (x y : A) : bool :=
+Definition nequiv_decb [ EqDec A ] (x y : A) : bool :=
   negb (equiv_decb x y).
 
 Infix "==b" := equiv_decb (no associativity, at level 70).
@@ -71,19 +71,19 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70).
 
 (** Decidable leibniz equality instances. *)
 
-Implicit Arguments eq [[A]].
-
 Require Import Coq.Arith.Arith.
 
-Program Instance nat_eqdec : EqDec nat eq :=
+(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
+
+Program Instance nat_eq_eqdec : ? EqDec (@eq_setoid nat) :=
   equiv_dec := eq_nat_dec.
 
 Require Import Coq.Bool.Bool.
 
-Program Instance bool_eqdec : EqDec bool eq :=
+Program Instance bool_eqdec : ? EqDec (@eq_setoid bool) :=
   equiv_dec := bool_dec.
 
-Program Instance unit_eqdec : EqDec unit eq :=
+Program Instance unit_eqdec : ? EqDec (@eq_setoid unit) :=
   equiv_dec x y := left.
 
   Next Obligation.
@@ -92,7 +92,8 @@ Program Instance unit_eqdec : EqDec unit eq :=
     reflexivity.
   Qed.
 
-Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : EqDec (prod A B) eq :=
+Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] => 
+  prod_eqdec : ? EqDec (@eq_setoid (prod A B)) :=
   equiv_dec x y := 
     dest x as (x1, x2) in 
     dest y as (y1, y2) in 
@@ -101,13 +102,11 @@ Program Instance [ EqDec A eq, EqDec B eq ] => prod_eqdec : EqDec (prod A B) eq
       else right
     else right.
 
-  Solve Obligations using unfold equiv ; program_simpl ; try red ; intros ; autoinjections ; discriminates.
-
 (** Objects of function spaces with countable domains like bool have decidable equality. *)
 
 Require Import Coq.Program.FunctionalExtensionality.
 
-Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq :=
+Program Instance [ ? EqDec (@eq_setoid A) ] => bool_function_eqdec : ? EqDec (@eq_setoid (bool -> A)) :=
   equiv_dec f g := 
     if f true == g true then
       if f false == g false then left
@@ -118,7 +117,6 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : EqDec (bool -> A) eq :=
 
   Next Obligation.
   Proof.
-    red.
     extensionality x.
     destruct x ; auto.
   Qed.