| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2009-03-28 | ZArith/Int: no need to load romega here (but rather in FullAVL) | letouzey | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12027 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2008-04-03 | New file FMapFullAVL containing the balancing proofs about FMapAVL: | letouzey | |
| 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 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |