diff options
| author | letouzey | 2008-04-03 18:28:26 +0000 |
|---|---|---|
| committer | letouzey | 2008-04-03 18:28:26 +0000 |
| commit | b8b0e5813a01a0a8e816ee30be1b626cffbeb092 (patch) | |
| tree | 0f6f7841efb8e99b7073fc0a725152d87139f701 /dev/base_include | |
| parent | ec3f3aed78e6c31ce819723a35efd68474d8c006 (diff) | |
New file FMapFullAVL containing the balancing proofs about FMapAVL:
As for FSetAVL vs. FSetFullAVL, preservation of the balancing of trees
is not necessary anymore for just fulfilling the Map interface. But we
still want theses proofs to exists somewhere, since they ensure the
correct efficiency of the FMapAVL operations.
In addition, FSetFullAVL also contains the non-structural,
ocaml-faithful version of compare.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10748 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions