aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes/Init.v
AgeCommit message (Expand)Author
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