aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetCompat.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Fix warning about shadowing a global name.Gravatar Gaëtan Gilbert2017-12-19
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* FSets/Msets: some renaming of module params to simplify the task of the extra...Gravatar letouzey2010-07-05
* CompSpecType, a clone of CompSpec but in Type instead of PropGravatar letouzey2010-02-12
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* Better visibility of the inductive CompSpec used to specify comparison functionsGravatar letouzey2009-11-03
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* FSetCompat: a compatibility wrapper between FSets and MSetsGravatar letouzey2009-10-20