Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 16 insertions, 19 deletions

diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 8a069343..bac64724 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -1,4 +1,3 @@
-(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -10,10 +9,10 @@
 (* 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: SetoidDec.v 11282 2008-07-28 11:51:53Z msozeau $ *)
+(* $Id: SetoidDec.v 11800 2009-01-18 18:34:15Z msozeau $ *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -27,12 +26,12 @@ Require Export Coq.Classes.SetoidClass.
 
 Require Import Coq.Logic.Decidable.
 
-Class DecidableSetoid A [ Setoid A ] :=
+Class DecidableSetoid `(S : Setoid A) :=
   setoid_decidable : forall x y : A, decidable (x == y).
 
 (** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
 
-Class (( s : Setoid A )) => EqDec :=
+Class EqDec `(S : Setoid A) :=
   equiv_dec : forall x y : A, { x == y } + { x =/= y }.
 
 (** We define the [==] overloaded notation for deciding equality. It does not take precedence
@@ -52,7 +51,7 @@ Open Local Scope program_scope.
 
 (** Invert the branches. *)
 
-Program Definition nequiv_dec [ EqDec A ] (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 +59,10 @@ Infix "=/=" := nequiv_dec (no associativity, at level 70).
 
 (** Define boolean versions, losing the logical information. *)
 
-Definition equiv_decb [ EqDec A ] (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 ] (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).
@@ -75,19 +74,19 @@ 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 :=
-  equiv := eq ; setoid_equiv := eq_equivalence.
+Program Instance eq_setoid A : Setoid A | 10 :=
+  { 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,8 +94,8 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
     reflexivity.
   Qed.
 
-Program Instance prod_eqdec [ ! EqDec (eq_setoid A), ! EqDec (eq_setoid B) ] : EqDec (eq_setoid (prod A B)) :=
-  equiv_dec x y := 
+Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) :=
+  λ x y,
     let '(x1, x2) := x in 
     let '(y1, y2) := y in 
     if x1 == y1 then 
@@ -108,10 +107,8 @@ Program Instance prod_eqdec [ ! EqDec (eq_setoid A), ! EqDec (eq_setoid B) ] : E
 
 (** Objects of function spaces with countable domains like bool have decidable equality. *)
 
-Require Import Coq.Program.FunctionalExtensionality.
-
-Program Instance bool_function_eqdec [ ! EqDec (eq_setoid A) ] : EqDec (eq_setoid (bool -> A)) :=
-  equiv_dec f g := 
+Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) :=
+  λ f g,
     if f true == g true then
       if f false == g false then in_left
       else in_right