aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/MSets')
-rw-r--r--theories/MSets/MSetEqProperties.v2
-rw-r--r--theories/MSets/MSetInterface.v2
-rw-r--r--theories/MSets/MSetList.v4
-rw-r--r--theories/MSets/MSetPositive.v40
-rw-r--r--theories/MSets/MSetRBT.v4
5 files changed, 26 insertions, 26 deletions
diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v
index 4f0d93fb9..843b9aaa7 100644
--- a/theories/MSets/MSetEqProperties.v
+++ b/theories/MSets/MSetEqProperties.v
@@ -856,7 +856,7 @@ intros.
rewrite <- (fold_equal _ _ _ _ fc ft 0 _ _ H).
rewrite <- (fold_equal _ _ _ _ gc gt 0 _ _ H).
rewrite <- (fold_equal _ _ _ _ fgc fgt 0 _ _ H); auto.
-intros; do 3 (rewrite fold_add; auto with *).
+intros. do 3 (rewrite fold_add; auto with *).
do 3 rewrite fold_empty;auto.
Qed.
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index bd8811689..a61ef8bcd 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -595,7 +595,7 @@ Module Raw2SetsOn (O:OrderedType)(M:RawSets O) <: SetsOn O.
(** Specification of [lt] *)
Instance lt_strorder : StrictOrder lt.
Proof. constructor ; unfold lt; red.
- unfold complement. red. intros. apply (irreflexivity H).
+ unfold complement. red. intros. apply (irreflexivity _ H).
intros. transitivity y; auto.
Qed.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index b0e09b719..5c232f340 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -472,7 +472,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
equal s s' = true <-> Equal s s'.
Proof.
induction s as [ | x s IH]; intros [ | x' s'] Hs Hs'; simpl.
- intuition.
+ intuition reflexivity.
split; intros H. discriminate. assert (In x' nil) by (rewrite H; auto). inv.
split; intros H. discriminate. assert (In x nil) by (rewrite <-H; auto). inv.
inv.
@@ -820,7 +820,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
Lemma compare_spec_aux : forall s s', CompSpec eq L.lt s s' (compare s s').
Proof.
- induction s as [|x s IH]; intros [|x' s']; simpl; intuition.
+ induction s as [|x s IH]; intros [|x' s']; simpl; intuition.
elim_compare x x'; auto.
Qed.
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index f3a1d39c9..25a8c1629 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -93,7 +93,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
Module E:=PositiveOrderedTypeBits.
- Definition elt := positive.
+ Definition elt := positive : Type.
Inductive tree :=
| Leaf : tree
@@ -101,9 +101,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
Scheme tree_ind := Induction for tree Sort Prop.
- Definition t := tree.
+ Definition t := tree : Type.
- Definition empty := Leaf.
+ Definition empty : t := Leaf.
Fixpoint is_empty (m : t) : bool :=
match m with
@@ -142,7 +142,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
(** helper function to avoid creating empty trees that are not leaves *)
- Definition node l (b: bool) r :=
+ Definition node (l : t) (b: bool) (r : t) : t :=
if b then Node l b r else
match l,r with
| Leaf,Leaf => Leaf
@@ -159,7 +159,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
end
end.
- Fixpoint union (m m': t) :=
+ Fixpoint union (m m': t) : t :=
match m with
| Leaf => m'
| Node l o r =>
@@ -169,7 +169,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
end
end.
- Fixpoint inter (m m': t) :=
+ Fixpoint inter (m m': t) : t :=
match m with
| Leaf => Leaf
| Node l o r =>
@@ -179,7 +179,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
end
end.
- Fixpoint diff (m m': t) :=
+ Fixpoint diff (m m': t) : t :=
match m with
| Leaf => Leaf
| Node l o r =>
@@ -211,7 +211,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
(** reverses [y] and concatenate it with [x] *)
- Fixpoint rev_append y x :=
+ Fixpoint rev_append (y x : elt) : elt :=
match y with
| 1 => x
| y~1 => rev_append y x~1
@@ -262,14 +262,14 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
end.
Definition exists_ m := xexists m 1.
- Fixpoint xfilter (m : t) (i : positive) :=
+ Fixpoint xfilter (m : t) (i : positive) : t :=
match m with
| Leaf => Leaf
| Node l o r => node (xfilter l i~0) (o &&& f (rev i)) (xfilter r i~1)
end.
Definition filter m := xfilter m 1.
- Fixpoint xpartition (m : t) (i : positive) :=
+ Fixpoint xpartition (m : t) (i : positive) : t * t :=
match m with
| Leaf => (Leaf,Leaf)
| Node l o r =>
@@ -311,7 +311,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
(** would it be more efficient to use a path like in the above functions ? *)
- Fixpoint choose (m: t) :=
+ Fixpoint choose (m: t) : option elt :=
match m with
| Leaf => None
| Node l o r => if o then Some 1 else
@@ -321,7 +321,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
end
end.
- Fixpoint min_elt (m: t) :=
+ Fixpoint min_elt (m: t) : option elt :=
match m with
| Leaf => None
| Node l o r =>
@@ -331,7 +331,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
end
end.
- Fixpoint max_elt (m: t) :=
+ Fixpoint max_elt (m: t) : option elt :=
match m with
| Leaf => None
| Node l o r =>
@@ -805,7 +805,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
rewrite <- andb_lazy_alt. apply andb_true_iff.
Qed.
- Lemma filter_spec: forall s x f, compat_bool E.eq f ->
+ Lemma filter_spec: forall s x f, @compat_bool elt E.eq f ->
(In x (filter f s) <-> In x s /\ f x = true).
Proof. intros. apply xfilter_spec. Qed.
@@ -830,7 +830,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
apply H. assumption.
Qed.
- Lemma for_all_spec: forall s f, compat_bool E.eq f ->
+ Lemma for_all_spec: forall s f, @compat_bool elt E.eq f ->
(for_all f s = true <-> For_all (fun x => f x = true) s).
Proof. intros. apply xforall_spec. Qed.
@@ -852,7 +852,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
intros [[x|x|] H]; eauto.
Qed.
- Lemma exists_spec : forall s f, compat_bool E.eq f ->
+ Lemma exists_spec : forall s f, @compat_bool elt E.eq f ->
(exists_ f s = true <-> Exists (fun x => f x = true) s).
Proof. intros. apply xexists_spec. Qed.
@@ -868,11 +868,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
destruct o; simpl; rewrite IHl, IHr; reflexivity.
Qed.
- Lemma partition_spec1 : forall s f, compat_bool E.eq f ->
+ Lemma partition_spec1 : forall s f, @compat_bool elt E.eq f ->
Equal (fst (partition f s)) (filter f s).
Proof. intros. rewrite partition_filter. reflexivity. Qed.
- Lemma partition_spec2 : forall s f, compat_bool E.eq f ->
+ Lemma partition_spec2 : forall s f, @compat_bool elt E.eq f ->
Equal (snd (partition f s)) (filter (fun x => negb (f x)) s).
Proof. intros. rewrite partition_filter. reflexivity. Qed.
@@ -1079,7 +1079,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
destruct (min_elt r).
injection H. intros <-. clear H.
destruct y as [z|z|].
- apply (IHr p z); trivial.
+ apply (IHr e z); trivial.
elim (Hp _ H').
discriminate.
discriminate.
@@ -1133,7 +1133,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
injection H. intros <-. clear H.
destruct y as [z|z|].
elim (Hp _ H').
- apply (IHl p z); trivial.
+ apply (IHl e z); trivial.
discriminate.
discriminate.
Qed.
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index f0cddcc38..d8f675ade 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -1047,7 +1047,7 @@ Qed.
(** ** Filter *)
-Lemma filter_app A f (l l':list A) :
+Polymorphic Lemma filter_app A f (l l':list A) :
List.filter f (l ++ l') = List.filter f l ++ List.filter f l'.
Proof.
induction l as [|x l IH]; simpl; trivial.
@@ -1196,7 +1196,7 @@ Lemma INV_rev l1 l2 acc :
Proof.
intros. rewrite rev_append_rev.
apply SortA_app with X.eq; eauto with *.
- intros x y. inA. eapply l1_lt_acc; eauto.
+ intros x y. inA. eapply @l1_lt_acc; eauto.
Qed.
(** ** union *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 14:39:25 +0000