diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-03 18:28:26 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-03 18:28:26 +0000 |
| commit | b8b0e5813a01a0a8e816ee30be1b626cffbeb092 (patch) | |
| tree | 0f6f7841efb8e99b7073fc0a725152d87139f701 /Makefile.common | |
| 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 'Makefile.common')
| -rw-r--r-- | Makefile.common | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.common b/Makefile.common index ddd13223e..2cecce059 100644 --- a/Makefile.common +++ b/Makefile.common @@ -620,7 +620,7 @@ FSETS_basic:= FSETS_all:=\ theories/FSets/FSetFullAVL.vo \ - theories/FSets/FMapAVL.vo + theories/FSets/FMapAVL.vo theories/FSets/FMapFullAVL.vo FSETSVO:=$(FSETSBASEVO) $(FSETS_$(FSETS)) |