aboutsummaryrefslogtreecommitdiff
path: root/tactics/class_setoid.ml4
AgeCommit message (Expand)Author
2008-02-13Move class_setoid to class_tactics.msozeau
2008-02-13Debugging of the class_setoid tactic and eauto. Prepare for move frommsozeau
2008-02-10Backport Program Instance into Instance. Proper early error message ifmsozeau
2008-02-09Fix the clrewrite tactic, change Relations.v to work on relations in Propmsozeau
2008-02-08Change implementation of resolution for typeclasses to use a customizedmsozeau
2008-02-06New algorithm to resolve morphisms, after discussion with Nicolasmsozeau
2008-02-03Add new files theories/Program/Basics.v and theories/Classes/Relations.vmsozeau
2008-01-30Support for occurences and 'in' in class_setoid, work on corresponding tactic...msozeau
2008-01-15Generalize instance declarations to any context, better name handling. Add ho...msozeau
2008-01-07Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...msozeau
2007-12-31Move Classes.Setoid to Classes.SetoidClass to avoid name clash.msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau