index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
theories
/
Classes
/
RelationPairs.v
Age
Commit message (
Expand
)
Author
2020-11-16
Merge PR #13384: Warn on hints without an explicit locality
coqbot-app[bot]
2020-11-16
Explicitly annotate all hint declarations of the standard library.
Pierre-Marie Pédrot
2020-11-15
Default disable automatic generalization of Instance type
Gaëtan Gilbert
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-01-24
Make `Instance` without a body always open a proof.
Maxime Dénès
2018-11-14
Deprecate hint declaration/removal with no specified database
Maxime Dénès
2018-02-27
Update headers following #6543.
Théo Zimmermann
2016-06-16
Typeclasses: stdlib fixes for new search algorithm
Matthieu Sozeau
2015-01-18
Remove typeclass opaque directive, some proofs in the stdlib rely on it being...
Matthieu Sozeau
2015-01-18
Optionally allow eta-conversion during unification for type classes.
Matthieu Sozeau
2014-05-06
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2011-11-21
theories/, plugins/ and test-suite/ ported to the Arguments vernacular
gareuselesinge
2011-03-13
- Add modulo_delta_types flag for unification to allow full
msozeau
2010-06-08
Made option "Automatic Introduction" active by default before too many
herbelin
2009-12-18
RelationPairs: stop loading it in all Numbers, stop maximal args with fst/snd
letouzey
2009-11-30
Fix backtracking heuristic in typeclass resolution.
msozeau
2009-11-06
Numbers: finish files NStrongRec and NDefOps
letouzey
2009-11-03
OrderedType implementation for various numerical datatypes + min/max structures
letouzey
