Fix obligations not being discharged due to new definition of complement.

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

1 files changed, 6 insertions, 2 deletions

diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 0a8623316..c385fc5b5 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -75,6 +75,9 @@ 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 : Setoid A :=
+  equiv := eq ; setoid_equiv := eq_equivalence.
+
 Program Instance nat_eq_eqdec : ? EqDec (@eq_setoid nat) :=
   equiv_dec := eq_nat_dec.
 
@@ -102,6 +105,8 @@ Program Instance [ ? EqDec (@eq_setoid A), ? EqDec (@eq_setoid B) ] =>
       else right
     else right.
 
+  Solve Obligations using unfold complement ; program_simpl.
+
 (** Objects of function spaces with countable domains like bool have decidable equality. *)
 
 Require Import Coq.Program.FunctionalExtensionality.
@@ -113,11 +118,10 @@ Program Instance [ ? EqDec (@eq_setoid A) ] => bool_function_eqdec : ? EqDec (@e
       else right
     else right.
 
-  Solve Obligations using try red ; unfold equiv ; program_simpl.
+  Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
 
   Next Obligation.
   Proof.
     extensionality x.
     destruct x ; auto.
   Qed.
-