aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/RelationPairs.v
Commit message (Expand)AuthorAge
* Typeclasses: stdlib fixes for new search algorithmGravatar Matthieu Sozeau2016-06-16
* Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Gravatar Matthieu Sozeau2015-01-18
* Optionally allow eta-conversion during unification for type classes.Gravatar Matthieu Sozeau2015-01-18
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* RelationPairs: stop loading it in all Numbers, stop maximal args with fst/sndGravatar letouzey2009-12-18
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* Numbers: finish files NStrongRec and NDefOpsGravatar letouzey2009-11-06
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 14:30:32 +0000