diff options
Diffstat (limited to 'theories/Lists/ListSet.v')
| -rw-r--r-- | theories/Lists/ListSet.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 20dc61ef18..77caa9c22b 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -20,7 +20,7 @@ Set Implicit Arguments. Section first_definitions. - Variable A : Set. + Variable A : Type. Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}. Definition set := list A. @@ -100,7 +100,7 @@ Section first_definitions. Qed. Lemma set_mem_ind : - forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set), + forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set), (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z). Proof. @@ -110,7 +110,7 @@ Section first_definitions. Qed. Lemma set_mem_ind2 : - forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set), + forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set), (set_In a x -> P y) -> (~ set_In a x -> P z) -> P (if set_mem a x then y else z). @@ -373,7 +373,7 @@ End first_definitions. Section other_definitions. - Variables A B : Set. + Variables A B : Type. Definition set_prod : set A -> set B -> set (A * B) := list_prod (A:=A) (B:=B). |