| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
| |
Contributed by Alexandre Ren, Damien Pous, and Thomas Braibant.
I've also included a MSets version, hence FSetPositive might become
soon a mere wrapper for MSetPositive, as for other FSets
implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13287 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
in */*/vo.itarget
On the way: no more -fsets (yes|no) and -reals (yes|no) option of configure
if you want a partial build, make a specific rule such as theories-light
Beware: these vo.itarget should not contain comments. Even if this is legal
for ocamlbuild, the $(shell cat ...) we do in Makefile can't accept that.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12574 85f007b7-540e-0410-9357-904b9bb8a0f7
|
letouzey