aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/ROrderedType.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Updating headers.Gravatar herbelin2012-08-08
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...Gravatar letouzey2010-01-07
* Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxiomsGravatar letouzey2009-11-16
* DecidableType: A specification via boolean equality as an alternative to eq_decGravatar letouzey2009-11-10
* ROrderedType + Rminmax : Coq's Reals can be seen as OrderedType.Gravatar letouzey2009-11-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 12:35:41 +0000