diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-10 15:38:59 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-10 15:38:59 +0000 |
| commit | a884f7dcebed71608f395fe140722790367089e2 (patch) | |
| tree | 942398bdde4d6419e25ca7bfd76aa9b150d7b54d /theories/Sorting | |
| parent | 43582a9c7ac7e5f2311c8ce52d8107553b2c9673 (diff) | |
isolate instances about Permutation and PermutationA which may slow rewrite
After discovering a rewrite in Ergo that takes a loooong time due
to a bad interaction with the instances of Permutation and PermutationA :
- PermutationA is now in a separate file SetoidPermutation
- File Permutation.v isn't Require'd by SetoidList anymore
nor MergeSort.v, just the definitions in Sorted.v
- Attempt to put a priority on these instances.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15584 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sorting')
| -rw-r--r-- | theories/Sorting/Permutation.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index fdfcd394a..eb769b77d 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -85,7 +85,7 @@ Instance Permutation_Equivalence A : Equivalence (@Permutation A) | 10 := { Equivalence_Transitive := @Permutation_trans A }. Instance Permutation_cons A : - Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A). + Proper (Logic.eq ==> @Permutation A ==> @Permutation A) (@cons A) | 10. Proof. repeat intro; subst; auto using perm_skip. Qed. @@ -106,7 +106,7 @@ Proof. Qed. Global Instance Permutation_in' : - Proper (Logic.eq ==> @Permutation A ==> iff) (@In A). + Proper (Logic.eq ==> @Permutation A ==> iff) (@In A) | 10. Proof. repeat red; intros; subst; eauto using Permutation_in. Qed. @@ -138,7 +138,7 @@ Proof. Qed. Global Instance Permutation_app' : - Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A). + Proper (@Permutation A ==> @Permutation A ==> @Permutation A) (@app A) | 10. Proof. repeat intro; now apply Permutation_app. Qed. @@ -187,7 +187,7 @@ Proof. Qed. Global Instance Permutation_rev' : - Proper (@Permutation A ==> @Permutation A) (@rev A). + Proper (@Permutation A ==> @Permutation A) (@rev A) | 10. Proof. repeat intro; now rewrite <- 2 Permutation_rev. Qed. @@ -199,7 +199,7 @@ Proof. Qed. Global Instance Permutation_length' : - Proper (@Permutation A ==> Logic.eq) (@length A). + Proper (@Permutation A ==> Logic.eq) (@length A) | 10. Proof. exact Permutation_length. Qed. @@ -407,7 +407,7 @@ Proof. Qed. Global Instance Permutation_NoDup' : - Proper (@Permutation A ==> iff) (@NoDup A). + Proper (@Permutation A ==> iff) (@NoDup A) | 10. Proof. repeat red; eauto using Permutation_NoDup. Qed. @@ -426,7 +426,7 @@ Proof. Qed. Global Instance Permutation_map' : - Proper (@Permutation A ==> @Permutation B) (map f). + Proper (@Permutation A ==> @Permutation B) (map f) | 10. Proof. exact Permutation_map. Qed. |