Avoid using a deprecated lemma in the standard library.

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.