diff options
Diffstat (limited to 'theories/MSets')
| -rw-r--r-- | theories/MSets/MSetPositive.v | 28 | ||||
| -rw-r--r-- | theories/MSets/MSetRBT.v | 4 |
2 files changed, 16 insertions, 16 deletions
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v index 8dd240f46..be95a0379 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 751d4f35c..83a2343dd 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. |