diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-06-26 17:38:23 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-06-26 17:38:23 +0200 |
| commit | f25ebf0a2d163df5191cf20650c82955b17972f7 (patch) | |
| tree | 7069e7b333355163268b7aeeabd0b5d0fe3ea23d /theories/FSets | |
| parent | cda7b80182b03c7b04baf5cc2cc6aa33984e054a (diff) | |
Avoid using a deprecated lemma in the standard library.
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 12 | ||||
| -rw-r--r-- | theories/FSets/FMapFullAVL.v | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 7f5853494..9e8f44c0f 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -1367,7 +1367,7 @@ Proof. induction s; simpl; intros; auto. rewrite IHs1, IHs2. unfold elements; simpl. - rewrite 2 IHs1, IHs2, <- !app_nil_end, !app_ass; auto. + rewrite 2 IHs1, IHs2, !app_nil_r, !app_ass; auto. Qed. Lemma elements_node : @@ -1376,7 +1376,7 @@ Lemma elements_node : elements (Node t1 x e t2 z) ++ l. Proof. unfold elements; simpl; intros. - rewrite !elements_app, <- !app_nil_end, !app_ass; auto. + rewrite !elements_app, !app_nil_r, !app_ass; auto. Qed. (** * Fold *) @@ -1491,9 +1491,9 @@ Lemma equal_IfEq : forall (m1 m2:t elt), IfEq (equal cmp m1 m2) (elements m1) (elements m2). Proof. intros; unfold equal. - rewrite (app_nil_end (elements m1)). + rewrite <- (app_nil_r (elements m1)). replace (elements m2) with (flatten_e (cons m2 (End _))) - by (rewrite cons_1; simpl; rewrite <-app_nil_end; auto). + by (rewrite cons_1; simpl; rewrite app_nil_r; auto). apply equal_cont_IfEq. intros. apply equal_end_IfEq; auto. @@ -2096,9 +2096,9 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Cmp (compare_pure s1 s2) (R.elements s1) (R.elements s2). Proof. intros; unfold compare_pure. - rewrite (app_nil_end (R.elements s1)). + rewrite <- (app_nil_r (R.elements s1)). replace (R.elements s2) with (P.flatten_e (R.cons s2 (R.End _))) by - (rewrite P.cons_1; simpl; rewrite <- app_nil_end; auto). + (rewrite P.cons_1; simpl; rewrite app_nil_r; auto). auto using compare_cont_Cmp, compare_end_Cmp. Qed. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 59b778369..dea23d68c 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -726,7 +726,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: intros. assert (H1:=cons_1 m1 (Raw.End _)). assert (H2:=cons_1 m2 (Raw.End _)). - simpl in *; rewrite <- app_nil_end in *; rewrite <-H1,<-H2. + simpl in *; rewrite app_nil_r in *; rewrite <-H1,<-H2. apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _))). Qed. |