aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Sorting/PermutSetoid.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-04 17:33:35 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-04 17:33:35 +0000
commit58c70113a815a42593c566f64f2de840fc7e48a1 (patch)
treec667f773ad8084832e54cebe46e6fabe07a9adeb /theories/Sorting/PermutSetoid.v
parent1f559440d19d9e27a3c935a26b6c8447c2220654 (diff)
migration from Set to Type of FSet/FMap + some dependencies...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10616 85f007b7-540e-0410-9357-904b9bb8a0f7
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.