aboutsummaryrefslogtreecommitdiff
path: root/theories/Structures/OrderedType.v
AgeCommit message (Expand)Author
2021-01-08Modify Structures/OrderedType.v to compile with -mangle-namesJasper Hugunin
2020-11-16Explicitly annotate all hint declarations of the standard library.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2015-12-07Fix some typos.Guillaume Melquiond
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-09Restore implicit arguments of irreflexivity (fixes bug #3305).Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2012-12-18Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)letouzey
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-01-31Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...msozeau
2012-01-28Tentative to fix bug #2628 by not letting intuition break records. Might be t...msozeau
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-07-26All the parameters of Compare are implicits.pboutill
2011-02-16Fix compilation issues.msozeau
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-01-17Simplification of OrdersTac thanks to the functor application ! with no inlineletouzey
2010-01-07Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*letouzey
2010-01-07Include can accept both Module and Module Typeletouzey
2010-01-07OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...letouzey
2009-11-03OrderedType implementation for various numerical datatypes + min/max structuresletouzey
2009-10-19Merge SetoidList2 into SetoidList.letouzey
2009-10-16Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...letouzey
2009-10-14Improved tactic "order" in OrderedTypeletouzey
2009-10-13MSets: a new generation of FSetsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:06:39 +0000