From cf7312a664465f44037a27cc7547b0e2d9f671a8 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 6 Feb 2008 17:04:18 +0000
Subject: 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
---
 theories/Classes/SetoidDec.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 0a86233166..c385fc5b5c 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.
-
-- 
cgit v1.2.3