aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/OrderedType.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Restore implicit arguments of irreflexivity (fixes bug #3305).Gravatar Matthieu Sozeau2014-05-09
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)Gravatar letouzey2012-12-18
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...Gravatar msozeau2012-01-31
* Tentative to fix bug #2628 by not letting intuition break records. Might be t...Gravatar msozeau2012-01-28
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* All the parameters of Compare are implicits.Gravatar pboutill2011-07-26
* Fix compilation issues.Gravatar msozeau2011-02-16
* - Fix treatment of globality flag for typeclass instance hints (theyGravatar msozeau2011-02-14
* 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
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Simplification of OrdersTac thanks to the functor application ! with no inlineGravatar letouzey2010-01-17
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...Gravatar letouzey2010-01-07
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...Gravatar letouzey2009-10-16
* Improved tactic "order" in OrderedTypeGravatar letouzey2009-10-14
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-22 00:17:40 +0000