diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-13 18:00:56 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-13 18:00:56 +0000 |
| commit | c8ec3774d0c4c17e23609fea45f517f678ba56df (patch) | |
| tree | 7874ffaaad78533e675d13c2fb25c9c7e29e57f9 /CHANGES | |
| parent | 317035368edd7c5af8b7d187155f5f7c536ab5d4 (diff) | |
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
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 7 |
1 files changed, 7 insertions, 0 deletions
@@ -42,6 +42,13 @@ Tactics - New command "r string" that interprets "idtac string" as a breakpoint and jumps to its next use in Ltac debugger. +Libraries + +- MSetRBT : a new implementation of MSets via Red-Black trees (initial + contribution by Andrew Appel). +- MSetAVL : for maximal sharing with the new MSetRBT, the argument order + of Node has changed (this should be transparent to regular MSets users). + Module System - The names of modules (and module types) are now in a fully separated |