diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-22 14:30:50 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-22 14:30:50 +0000 |
| commit | 78143a31a5a3f4a183b7e5a700567a51929f7fee (patch) | |
| tree | e74428a5616b3fae5b607b6280c4d8253b3c962b /theories/Sorting | |
| parent | d08282cb2242d642d8ea40e844dbe61b7404674c (diff) | |
Permutation: remove a compatibility notation which doesn't help MathClasses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15341 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/Permutation.v | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index c1d25a428..fdfcd394a 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -87,7 +87,7 @@ Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := { Instance Permutation_cons A : Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A). Proof. - repeat red; intros; subst; auto using perm_skip. + repeat intro; subst; auto using perm_skip. Qed. Section Permutation_properties. @@ -108,7 +108,7 @@ Qed. Global Instance Permutation_in' : Proper (Logic.eq ==> @Permutation A ==> iff) (@In A). Proof. - repeat red; intros; subst; eauto using Permutation_in. + repeat red; intros; subst; eauto using Permutation_in. Qed. Lemma Permutation_app_tail : forall (l l' tl : list A), @@ -140,7 +140,7 @@ Qed. Global Instance Permutation_app' : Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A). Proof. - repeat red; intros; now apply Permutation_app. + repeat intro; now apply Permutation_app. Qed. Lemma Permutation_add_inside : forall a (l l' tl tl' : list A), @@ -189,7 +189,7 @@ Qed. Global Instance Permutation_rev' : Proper (@Permutation A ==> @Permutation A) (@rev A). Proof. - repeat red; intros; now rewrite <- 2 Permutation_rev. + repeat intro; now rewrite <- 2 Permutation_rev. Qed. Theorem Permutation_length : forall (l l' : list A), @@ -201,7 +201,7 @@ Qed. Global Instance Permutation_length' : Proper (@Permutation A ==> Logic.eq) (@length A). Proof. - repeat red; now apply Permutation_length. + exact Permutation_length. Qed. Theorem Permutation_ind_bis : @@ -641,5 +641,4 @@ End Permutation_alt. (* begin hide *) Notation Permutation_app_swap := Permutation_app_comm (only parsing). -Notation Permutation_map_aux_Proper := Permutation_map' (only parsing). (* end hide *) |