aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes/RelationPairs.v
AgeCommit message (Expand)Author
2018-02-27Update headers following #6543.Théo Zimmermann
2016-06-16Typeclasses: stdlib fixes for new search algorithmMatthieu Sozeau
2015-01-18Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Matthieu Sozeau
2015-01-18Optionally allow eta-conversion during unification for type classes.Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2010-06-08Made option "Automatic Introduction" active by default before too manyherbelin
2009-12-18RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndletouzey
2009-11-30Fix backtracking heuristic in typeclass resolution. msozeau
2009-11-06Numbers: finish files NStrongRec and NDefOpsletouzey
2009-11-03OrderedType implementation for various numerical datatypes + min/max structuresletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 04:25:26 +0000