diff options
| -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 40f1f96c3a..ab1fc1ca69 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) := |