aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists/SetoidPermutation.v
Commit message (Collapse)AuthorAge
* isolate instances about Permutation and PermutationA which may slow rewriteGravatar letouzey2012-07-10
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