aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/OrdersFacts.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Little addition to 6eede071 for consistency of style in OrdersFacts.v.Gravatar Hugo Herbelin2016-10-12
* Further "decide equality" tests on demand of Jason.Gravatar Hugo Herbelin2016-09-17
* Extending "contradiction" so that it recognizes statements such as "~x=x" or ...Gravatar Hugo Herbelin2016-09-15
* Put implicits back as in 8.4.Gravatar Matthieu Sozeau2015-12-31
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Follow-up concerning eqb / ltb / leb comparisonsGravatar letouzey2011-06-21
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* CompSpecType, a clone of CompSpec but in Type instead of PropGravatar letouzey2010-02-12
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 16:20:44 +0000