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 | |
parent | cda7b80182b03c7b04baf5cc2cc6aa33984e054a (diff) |
Avoid using a deprecated lemma in the standard library.
-rw-r--r-- | theories/FSets/FMapAVL.v | 12 | ||||
-rw-r--r-- | theories/FSets/FMapFullAVL.v | 2 | ||||
-rw-r--r-- | theories/Lists/SetoidList.v | 2 | ||||
-rw-r--r-- | theories/MSets/MSetGenTree.v | 4 | ||||
-rw-r--r-- | theories/MSets/MSetRBT.v | 2 | ||||
-rw-r--r-- | theories/Sorting/PermutSetoid.v | 2 | ||||
-rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 2 |
7 files changed, 13 insertions, 13 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. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 0e56a96bd..e82277a45 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -762,7 +762,7 @@ Qed. Global Instance rev_eqlistA_compat : Proper (eqlistA==>eqlistA) (@rev A). Proof. repeat red. intros. -rewrite (app_nil_end (rev x)), (app_nil_end (rev y)). +rewrite <- (app_nil_r (rev x)), <- (app_nil_r (rev y)). apply eqlistA_rev_app; auto. Qed. diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 2ec125427..320ced06c 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -1063,9 +1063,9 @@ Lemma compare_Cmp : forall s1 s2, Cmp (compare s1 s2) (elements s1) (elements s2). Proof. intros; unfold compare. - rewrite (app_nil_end (elements s1)). + rewrite <- (app_nil_r (elements s1)). replace (elements s2) with (flatten_e (cons s2 End)) by - (rewrite cons_1; simpl; rewrite <- app_nil_end; auto). + (rewrite cons_1; simpl; rewrite app_nil_r; auto). apply compare_cont_Cmp; auto. intros. apply compare_end_Cmp; auto. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index ed09030cb..b79afc616 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -979,7 +979,7 @@ Proof. { transitivity size; trivial. subst. auto with arith. } destruct acc1 as [|x acc1]. { exfalso. revert LE. apply Nat.lt_nge. subst. - rewrite <- app_nil_end, <- elements_cardinal; auto with arith. } + rewrite app_nil_r, <- elements_cardinal; auto with arith. } specialize (Hg acc1). destruct (g acc1) as (t2,acc2). destruct Hg as (Hg1,Hg2). diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index 66185ce9c..1f25f4148 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -179,7 +179,7 @@ Proof. simpl; trivial using permut_refl. simpl. apply permut_add_cons_inside. - rewrite <- app_nil_end. trivial. + rewrite app_nil_r. trivial. Qed. (** * Some inversion results. *) diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 28288c0cb..d5e807f5a 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -183,7 +183,7 @@ Section Wf_Lexicographic_Exponentiation. intro. generalize (app_nil_end x1). - simple induction 1; simple induction 1. + simple induction 1; simple induction 1. split. apply d_conc; auto with sets. apply d_nil. |