diff options
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapFacts.v | 4 | ||||
| -rw-r--r-- | theories/FSets/FMapPositive.v | 8 | ||||
| -rw-r--r-- | theories/FSets/FSetPositive.v | 28 |
3 files changed, 20 insertions, 20 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index e68bc5930d..153842654a 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -1988,7 +1988,7 @@ Module OrdProperties (M:S). simpl; intros; try discriminate. intros. destruct a; destruct l; simpl in *. - injection H as -> ->. + injection H as [= -> ->]. inversion_clear H1. red in H; simpl in *; intuition. elim H0; eauto. @@ -2052,7 +2052,7 @@ Module OrdProperties (M:S). generalize (elements_3 m). destruct (elements m). try discriminate. - destruct p; injection H as -> ->; intros H4. + destruct p; injection H as [= -> ->]; intros H4. inversion_clear H1 as [? ? H2|? ? H2]. red in H2; destruct H2; simpl in *; ME.order. inversion_clear H4. rename H1 into H3. diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index b47c99244b..37dd2304da 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -277,7 +277,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. rewrite append_assoc_1; apply in_or_app; right; apply in_cons; apply IHm2; auto. rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. - rewrite append_neutral_r; apply in_or_app; injection H as ->; + rewrite append_neutral_r; apply in_or_app; injection H as [= ->]; right; apply in_eq. rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto. rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. @@ -318,7 +318,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. apply in_or_app. left; apply IHm1; auto. right; destruct (in_inv H0). - injection H1 as -> ->; apply in_eq. + injection H1 as [= -> ->]; apply in_eq. apply in_cons; apply IHm2; auto. left; apply IHm1; auto. right; apply IHm2; auto. @@ -349,7 +349,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. apply in_or_app. left; apply IHm1; auto. right; destruct (in_inv H0). - injection H1 as -> ->; apply in_eq. + injection H1 as [= -> ->]; apply in_eq. apply in_cons; apply IHm2; auto. left; apply IHm1; auto. right; apply IHm2; auto. @@ -692,7 +692,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst. red; red; simpl. destruct H0. - injection H0 as H0 _; subst. + injection H0 as [= H0 _]; subst. eapply xelements_bits_lt_1; eauto. apply E.bits_lt_trans with p. eapply xelements_bits_lt_1; eauto. diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v index 8a93f38164..d2e10e42a6 100644 --- a/theories/FSets/FSetPositive.v +++ b/theories/FSets/FSetPositive.v @@ -1009,10 +1009,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 as <-. apply Hp. + intros p Hp x [= <-]. apply Hp. reflexivity. intros _ x. revert IHr. case choose. - intros p Hp H. injection H as <-. apply Hp. + intros p Hp [= <-]. apply Hp. reflexivity. intros. discriminate. Qed. @@ -1068,11 +1068,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 as <-. apply IHl. reflexivity. + injection H as [= <-]. apply IHl. reflexivity. destruct o; simpl. - injection H as <-. reflexivity. + injection H as [= <-]. reflexivity. destruct (min_elt r); simpl in *. - injection H as <-. apply IHr. reflexivity. + injection H as [= <-]. apply IHr. reflexivity. discriminate. Qed. @@ -1096,15 +1096,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 as <-. + 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_3 in Hp. destruct o. - injection H as <-. intros Hl. + injection H as [= <-]. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (min_elt r). - injection H as <-. + injection H as [= <-]. destruct y as [z|z|]. apply (IHr e z); trivial. elim (Hp _ H'). @@ -1121,11 +1121,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 as <-. apply IHr. reflexivity. + injection H as [= <-]. apply IHr. reflexivity. destruct o; simpl. - injection H as <-. reflexivity. + injection H as [= <-]. reflexivity. destruct (max_elt l); simpl in *. - injection H as <-. apply IHl. reflexivity. + injection H as [= <-]. apply IHl. reflexivity. discriminate. Qed. @@ -1149,15 +1149,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 as <-. + 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_3 in Hp. destruct o. - injection H as <-. intros Hl. + injection H as [= <-]. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (max_elt l). - injection H as <-. + injection H as [= <-]. destruct y as [z|z|]. elim (Hp _ H'). apply (IHl e z); trivial. |