diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-23 22:11:25 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-23 22:11:25 +0000 |
| commit | 95dd7304f68eb155f572bf221c4d99fca85b700c (patch) | |
| tree | 8e78cb9ed1eee1939b327cbc0d013f8a99ea4570 /theories/Classes/SetoidDec.v | |
| parent | 32c11b16f7d7ff0ea3aee584103bd60f5b94dedb (diff) | |
Fix a bug found by B. Grégoire when declaring morphisms in module
types. Change (again) the semantics of bindings and the binding modifier
! in typeclasses. Inside [ ], implicit binding where only parameters
need to be given is the default, use ! to use explicit binding, which is
equivalent to regular bindings except for generalization of free
variables. Outside brackets (e.g. on the right of instance
declarations), explicit binding is the default, and implicit binding
can be used by adding ! in front. This avoids almost every use of ! in
the standard library and in other examples I have.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10713 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidDec.v')
| -rw-r--r-- | theories/Classes/SetoidDec.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 86a2bef80..26e1ab244 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -54,7 +54,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. *) @@ -62,10 +62,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). @@ -97,7 +97,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) := reflexivity. Qed. -Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] => +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 @@ -113,7 +113,7 @@ Program Instance [ EqDec (@eq_setoid A), EqDec (@eq_setoid B) ] => Require Import Coq.Program.FunctionalExtensionality. -Program Instance [ EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) := +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 in_left |