aboutsummaryrefslogtreecommitdiff
path: root/theories/Program
AgeCommit message (Expand)Author
2008-03-15Do a second pass on the treatment of user-given implicit arguments. Nowmsozeau
2008-03-08Fix bugs that were reopened due to the change of setoidmsozeau
2008-03-06Syntax changes in typeclasses, remove "?" for usual implicit argumentsmsozeau
2008-02-26Proper implicit arguments handling for assumptionsmsozeau
2008-02-13Debugging of the class_setoid tactic and eauto. Prepare for move frommsozeau
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-31Debug implementation of dependent induction/dependent destruction and documen...msozeau
2008-01-30Work on dependent induction tactic and friends, finish the test-suite examplemsozeau
2008-01-18Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...msozeau
2008-01-15Generalize instance declarations to any context, better name handling. Add ho...msozeau
2008-01-05Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...msozeau
2008-01-02Implicit arguments in class field declarationsmsozeau
2008-01-02Better resolution of implicit parameters in typeclass binders, add extensiona...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-10-24Addition of more general tactics for equality. Functional extensionality and ...msozeau
2007-08-26Add more equality tactics. Upgrade program_simpl for discrimination of conjun...msozeau
2007-08-08A better Program documentation. Include it in the generated stdlib doc.msozeau
2007-08-07Move Program tactics into a proper theories/ directory as they are general pu...msozeau