From f25ebf0a2d163df5191cf20650c82955b17972f7 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 26 Jun 2014 17:38:23 +0200 Subject: Avoid using a deprecated lemma in the standard library. --- theories/Sorting/PermutSetoid.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Sorting') 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. *) -- cgit v1.2.3