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