aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/EqualitiesFacts.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Revert "Temporary hack to compensate missing comma while re-printing tactic"Gravatar Hugo Herbelin2016-04-27
* Temporary hack to compensate missing comma while re-printing tacticGravatar Hugo Herbelin2016-04-27
* MMaps: remove it from final 8.5 release, since this new library isn't mature ...Gravatar Pierre Letouzey2016-01-13
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* MMaps again : adding MMapList, an implementation by ordered listGravatar Pierre Letouzey2015-03-05
* Introducing MMaps, a modernized FMaps.Gravatar Pierre Letouzey2015-03-04
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Numbers and bitwise functions.Gravatar letouzey2010-12-06
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07