index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
FSets
/
FSetAVL.v
Commit message (
Expand
)
Author
Age
*
* For uniformity, FSetAVL uses Implicit Arguments (a bit)
letouzey
2007-06-07
*
As suggested by Pierre Casteran, fold for FSets/FMaps now takes a
letouzey
2007-05-27
*
fix for bug #1347 (no more Scope pollution by FSets)
letouzey
2007-05-25
*
FSetInterface: new item choose_equal in the spec S (request of P. Casteran)
letouzey
2007-02-28
*
Passage des graphes de Function dans Type
jforest
2006-06-23
*
+ ameliorating the tactic "functional induction"
jforest
2006-06-06
*
Replacing the old version of "functional induction" with the new one.
jforest
2006-05-31
*
Suite changement précédence by de assert
herbelin
2006-05-24
*
suite des marquages de types et opacifications de lemmes dans les wrappers Make
letouzey
2006-05-22
*
suite tentative pour permettre l'utilisation de modules de FSets
letouzey
2006-05-20
*
suite de l'ajout des FSets/FMaps dans les theories standards
letouzey
2006-04-29
*
suppression de FSets (redevient une contrib)
filliatr
2003-06-24
*
doc
filliatr
2003-06-24
*
concat; debut split
filliatr
2003-06-24
*
join
filliatr
2003-06-23
*
add_tree : sur type tree plutot que sur type t
filliatr
2003-06-23
*
merge_bis et debug join
filliatr
2003-06-23
*
remov
filliatr
2003-06-20
*
merge
filliatr
2003-06-20
*
remove_min, remove_max
filliatr
2003-06-20
*
add
filliatr
2003-06-19
*
bal: preuve terminee
filliatr
2003-06-19
*
bal: premier cas hl > hr + 2
filliatr
2003-06-19
*
typo
filliatr
2003-06-19
*
AVL: suite
filliatr
2003-06-18
*
AVL: suite
filliatr
2003-06-17
*
AVL de caml: un debut
filliatr
2003-06-17