From c8ec3774d0c4c17e23609fea45f517f678ba56df Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 13 Apr 2012 18:00:56 +0000 Subject: MSetRBT : implementation of MSets via Red-Black trees Initial contribution by Andrew Appel, many ulterior modifications by myself. Interest: red-black trees maintain logarithmic depths as AVL, but they do not rely on integer height annotations as AVL, allowing interesting performance when computing in Coq or after standard extraction. More on this topic in the article by A. Appel. The common parts of MSetAVL and MSetRBT are shared in a new file MSetGenTree which include the definition of tree and functions such as mem fold elements compare subset. Note that the height of AVL trees is now the first arg of the Node constructor instead of the last one. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15168 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/stdlib/index-list.html.template | 2 ++ 1 file changed, 2 insertions(+) (limited to 'doc/stdlib') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index d688124d01..1541e90664 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -466,7 +466,9 @@ through the Require Import command.

theories/MSets/MSetEqProperties.v theories/MSets/MSetWeakList.v theories/MSets/MSetList.v + theories/MSets/MSetGenTree.v theories/MSets/MSetAVL.v + theories/MSets/MSetRBT.v theories/MSets/MSetPositive.v theories/MSets/MSetToFiniteSet.v (theories/MSets/MSets.v) -- cgit v1.2.3