aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Sorting/PermutSetoid.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sorting/PermutSetoid.v')
-rw-r--r--theories/Sorting/PermutSetoid.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v
index 84eac9905..e012bde19 100644
--- a/theories/Sorting/PermutSetoid.v
+++ b/theories/Sorting/PermutSetoid.v
@@ -23,7 +23,7 @@ Set Implicit Arguments.
Section Perm.
-Variable A : Set.
+Variable A : Type.
Variable eqA : relation A.
Hypothesis eqA_dec : forall x y:A, {eqA x y} + {~ eqA x y}.
@@ -198,7 +198,7 @@ Proof.
Qed.
-Variable B : Set.
+Variable B : Type.
Variable eqB : B->B->Prop.
Variable eqB_dec : forall x y:B, { eqB x y }+{ ~eqB x y }.
Variable eqB_trans : forall x y z, eqB x y -> eqB y z -> eqB x z.