diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-04 18:39:28 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-12-04 18:39:28 +0000 |
| commit | aa7a7c2fa5657cd6a279475dfd6adb77e26d2eaa (patch) | |
| tree | 63c18da345306df4c97b574dd86e90f95a55b85b /theories/Classes/SetoidDec.v | |
| parent | a282e9f8d18b1dcf9dd46900b0af522f8e46d8ef (diff) | |
Fix priority of the Leibniz Setoid instance to 10 (thanks to M. Lasson
for the report).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11656 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidDec.v')
| -rw-r--r-- | theories/Classes/SetoidDec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 40f1f96c3..ab1fc1ca6 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -74,7 +74,7 @@ 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 := +Program Instance eq_setoid A : Setoid A | 10 := equiv := eq ; setoid_equiv := eq_equivalence. Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) := |