aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetFullAVL.v
Commit message (Expand)AuthorAge
* FSetCompat: a compatibility wrapper between FSets and MSetsGravatar letouzey2009-10-20
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* ZArith/Int: no need to load romega here (but rather in FullAVL)Gravatar letouzey2009-03-28
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...Gravatar letouzey2008-12-17
* - notations &&& and ||| equivalent to andb and orb, Gravatar letouzey2008-03-27
* One more AVL reorganisation: separate pure functions from proofs + functional...Gravatar letouzey2008-03-21
* still some useless invariants in FSetAVLGravatar letouzey2008-03-20
* Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)Gravatar letouzey2008-03-15