From a884f7dcebed71608f395fe140722790367089e2 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 10 Jul 2012 15:38:59 +0000 Subject: 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 --- doc/stdlib/index-list.html.template | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/stdlib') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 6ad232b5f..0f21c082b 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -411,6 +411,7 @@ through the Require Import command.

theories/Lists/List.v theories/Lists/ListSet.v theories/Lists/SetoidList.v + theories/Lists/SetoidPermutation.v theories/Lists/Streams.v theories/Lists/StreamMemo.v theories/Lists/ListTactics.v -- cgit v1.2.3