summaryrefslogtreecommitdiff
path: root/theories/MSets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/MSets')
-rw-r--r--theories/MSets/MSetAVL.v1
-rw-r--r--theories/MSets/MSetDecide.v19
-rw-r--r--theories/MSets/MSetInterface.v3
-rw-r--r--theories/MSets/MSetList.v2
-rw-r--r--theories/MSets/MSetPositive.v28
-rw-r--r--theories/MSets/MSetRBT.v4
-rw-r--r--theories/MSets/MSetWeakList.v2
7 files changed, 27 insertions, 32 deletions
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index cc023cc3..a3c265a2 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -417,6 +417,7 @@ Local Open Scope Int_scope.
Let's do its job by hand: *)
Ltac join_tac :=
+ let l := fresh "l" in
intro l; induction l as [| lh ll _ lx lr Hlr];
[ | intros x r; induction r as [| rh rl Hrl rx rr _]; unfold join;
[ | destruct ((rh+2) <? lh) eqn:LT;
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index f2555791..9c622fd7 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -357,17 +357,8 @@ the above form:
| _ => idtac
end.
- (** [if t then t1 else t2] executes [t] and, if it does not
- fail, then [t1] will be applied to all subgoals
- produced. If [t] fails, then [t2] is executed. *)
- Tactic Notation
- "if" tactic(t)
- "then" tactic(t1)
- "else" tactic(t2) :=
- first [ t; first [ t1 | fail 2 ] | t2 ].
-
Ltac abstract_term t :=
- if (is_var t) then fail "no need to abstract a variable"
+ tryif (is_var t) then fail "no need to abstract a variable"
else (let x := fresh "x" in set (x := t) in *; try clearbody x).
Ltac abstract_elements :=
@@ -478,11 +469,11 @@ the above form:
repeat (
match goal with
| H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
- if (change T with E.t in H) then fail
- else if (change T with t in H) then fail
+ tryif (change T with E.t in H) then fail
+ else tryif (change T with t in H) then fail
else clear H
| H : ?P |- _ =>
- if prop (MSet_Prop P) holds by
+ tryif prop (MSet_Prop P) holds by
(auto 100 with MSet_Prop)
then fail
else clear H
@@ -747,7 +738,7 @@ the above form:
| H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
contradict H; fsetdec_body
| H: ?P -> False |- ?Q -> False =>
- if prop (MSet_elt_Prop P) holds by
+ tryif prop (MSet_elt_Prop P) holds by
(auto 100 with MSet_Prop)
then (contradict H; fsetdec_body)
else fsetdec_body
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index bd881168..74a7f6df 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -345,6 +345,9 @@ Module Type WRawSets (E : DecidableType).
predicate [Ok]. If [Ok] isn't decidable, [isok] may be the
always-false function. *)
Parameter isok : t -> bool.
+ (** MS:
+ Dangerous instance, the [isok s = true] hypothesis cannot be discharged
+ with typeclass resolution. Is it really an instance? *)
Declare Instance isok_Ok s `(isok s = true) : Ok s | 10.
(** Logical predicates *)
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index fb0d1ad9..05c20eb8 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -8,7 +8,7 @@
(** * Finite sets library *)
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
interface [MSetInterface.S] using strictly ordered list. *)
Require Export MSetInterface OrdersFacts OrdersLists.
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index 8dd240f4..be95a037 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -908,10 +908,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
destruct o.
intros x H. injection H; intros; subst. reflexivity.
revert IHl. case choose.
- intros p Hp x H. injection H; intros; subst; clear H. apply Hp.
+ intros p Hp x H. injection H as <-. apply Hp.
reflexivity.
intros _ x. revert IHr. case choose.
- intros p Hp H. injection H; intros; subst; clear H. apply Hp.
+ intros p Hp H. injection H as <-. apply Hp.
reflexivity.
intros. discriminate.
Qed.
@@ -968,11 +968,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
induction s as [| l IHl o r IHr]; simpl.
intros. discriminate.
intros x. destruct (min_elt l); intros.
- injection H. intros <-. apply IHl. reflexivity.
+ injection H as <-. apply IHl. reflexivity.
destruct o; simpl.
- injection H. intros <-. reflexivity.
+ injection H as <-. reflexivity.
destruct (min_elt r); simpl in *.
- injection H. intros <-. apply IHr. reflexivity.
+ injection H as <-. apply IHr. reflexivity.
discriminate.
Qed.
@@ -996,15 +996,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
induction s as [|l IHl o r IHr]; intros x y H H'.
discriminate.
simpl in H. case_eq (min_elt l).
- intros p Hp. rewrite Hp in H. injection H; intros <-.
+ intros p Hp. rewrite Hp in H. injection H as <-.
destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial.
intro Hp; rewrite Hp in H. apply min_elt_spec3 in Hp.
destruct o.
- injection H. intros <- Hl. clear H.
+ injection H as <-. intros Hl.
destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
destruct (min_elt r).
- injection H. intros <-. clear H.
+ injection H as <-.
destruct y as [z|z|].
apply (IHr e z); trivial.
elim (Hp _ H').
@@ -1021,11 +1021,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
induction s as [| l IHl o r IHr]; simpl.
intros. discriminate.
intros x. destruct (max_elt r); intros.
- injection H. intros <-. apply IHr. reflexivity.
+ injection H as <-. apply IHr. reflexivity.
destruct o; simpl.
- injection H. intros <-. reflexivity.
+ injection H as <-. reflexivity.
destruct (max_elt l); simpl in *.
- injection H. intros <-. apply IHl. reflexivity.
+ injection H as <-. apply IHl. reflexivity.
discriminate.
Qed.
@@ -1049,15 +1049,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
induction s as [|l IHl o r IHr]; intros x y H H'.
discriminate.
simpl in H. case_eq (max_elt r).
- intros p Hp. rewrite Hp in H. injection H; intros <-.
+ intros p Hp. rewrite Hp in H. injection H as <-.
destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial.
intro Hp; rewrite Hp in H. apply max_elt_spec3 in Hp.
destruct o.
- injection H. intros <- Hl. clear H.
+ injection H as <-. intros Hl.
destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
destruct (max_elt l).
- injection H. intros <-. clear H.
+ injection H as <-.
destruct y as [z|z|].
elim (Hp _ H').
apply (IHl e z); trivial.
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index 751d4f35..83a2343d 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -911,7 +911,7 @@ Proof.
{ inversion_clear O.
assert (InT x l) by now apply min_elt_spec1. auto. }
simpl. case X.compare_spec; try order.
- destruct lc; injection E; clear E; intros; subst l s0; auto.
+ destruct lc; injection E; subst l s0; auto.
Qed.
Lemma remove_min_spec1 s x s' `{Ok s}:
@@ -1948,7 +1948,7 @@ Module Make (X: Orders.OrderedType) <:
generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs).
set (P := Raw.remove_min_ok s). clearbody P.
destruct (Raw.remove_min s) as [(x0,s0)|]; try easy.
- intros H U. injection U. clear U; intros; subst. simpl.
+ intros H U. injection U as -> <-. simpl.
destruct (H x s0); auto. subst; intuition.
Qed.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 372acd56..2ac57a93 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -8,7 +8,7 @@
(** * Finite sets library *)
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
interface [MSetWeakInterface.S] using lists without redundancy. *)
Require Import MSetInterface.
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-28 04:01:27 +0000