| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
| |
but with lazy behavior while (vm_)computing
- FSetAVL.split has now a dedicated output type instead of ( ,( , ))
- Some proof adaptations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
functional scheme.
- Proofs are placed in Raw.Proofs, that may someday become an opaque module.
- use Functional Scheme in this module Raw.proofs, instead of Function: less
derived objects.
- more cleanup.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10707 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10701 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* FSetAVL is greatly lightened : modulo a minor change in bal, formal
proofs of avl invariant is not needed for building a functor
implementing FSetInterface.S (even if this invariant is still true)
* Non-structural functions (union, subset, compare, equal) are
transformed into efficient structural versions
* Both proofs of avl preservation and non-structural functions are
moved to a new file FSetFullAVL, that can be ignored by the average
user.
Same for FMapAVL (still work in progress...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10679 85f007b7-540e-0410-9357-904b9bb8a0f7
|