aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes/Init.v
AgeCommit message (Expand)Author
2009-09-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-05-16Minor fixes in typeclasses:msozeau
2009-04-27- Implementation of a new typeclasses eauto procedure based on successmsozeau
2009-04-16Better Requires in Classes. Fix bug #2093: the code does not requiremsozeau
2008-12-16Finish fix for the treatment of [inverse] in [setoid_rewrite], making amsozeau
2008-10-23Fix bug #1977 by allowing the [apply] variants to take an [open_constr]msozeau
2008-08-23Fix dependency problem that makes compilation fail :)msozeau
2008-08-22- New auto hints for transparency/opacity control, not bound to msozeau
2008-08-21Fixes in dependent induction tactic to keep names, allow givingmsozeau
2008-07-22New tactics [conv] to test convertibility (actually, unification) of twomsozeau
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-02-26Proper implicit arguments handling for assumptionsmsozeau
2008-02-08Change implementation of resolution for typeclasses to use a customizedmsozeau
2008-02-06New algorithm to resolve morphisms, after discussion with Nicolasmsozeau
2008-01-18Change notation for setoid inequality, coerce objects before comparing them. ...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau