index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Structures
/
OrderedType.v
Commit message (
Expand
)
Author
Age
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
Fix some typos.
Guillaume Melquiond
2015-12-07
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
*
Making those proofs which depend on names generated for the arguments
Hugo Herbelin
2014-06-01
*
Restore implicit arguments of irreflexivity (fixes bug #3305).
Matthieu Sozeau
2014-05-09
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Rework of GenericMinMax and OrdersTac (helps extraction, cf. #2904)
letouzey
2012-12-18
*
Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).
herbelin
2012-04-15
*
Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...
msozeau
2012-01-31
*
Tentative to fix bug #2628 by not letting intuition break records. Might be t...
msozeau
2012-01-28
*
theories/, plugins/ and test-suite/ ported to the Arguments vernacular
gareuselesinge
2011-11-21
*
All the parameters of Compare are implicits.
pboutill
2011-07-26
*
Fix compilation issues.
msozeau
2011-02-16
*
- Fix treatment of globality flag for typeclass instance hints (they
msozeau
2011-02-14
*
Reverted 13293 commited mistakenly. Sorry for the noise.
herbelin
2010-07-18
*
Tentative de suppression de l'import automatique des hints et coercions.
herbelin
2010-07-18
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Simplification of OrdersTac thanks to the functor application ! with no inline
letouzey
2010-01-17
*
Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*
letouzey
2010-01-07
*
Include can accept both Module and Module Type
letouzey
2010-01-07
*
OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...
letouzey
2010-01-07
*
OrderedType implementation for various numerical datatypes + min/max structures
letouzey
2009-11-03
*
Merge SetoidList2 into SetoidList.
letouzey
2009-10-19
*
Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...
letouzey
2009-10-16
*
Improved tactic "order" in OrderedType
letouzey
2009-10-14
*
MSets: a new generation of FSets
letouzey
2009-10-13