aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program
Commit message (Expand)AuthorAge
* Debugging of the class_setoid tactic and eauto. Prepare for move fromGravatar msozeau2008-02-13
* New algorithm to resolve morphisms, after discussion with NicolasGravatar msozeau2008-02-06
* Add new files theories/Program/Basics.v and theories/Classes/Relations.vGravatar msozeau2008-02-03
* Debug implementation of dependent induction/dependent destruction and documen...Gravatar msozeau2008-01-31
* Work on dependent induction tactic and friends, finish the test-suite exampleGravatar msozeau2008-01-30
* Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...Gravatar msozeau2008-01-18
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...Gravatar msozeau2008-01-05
* Implicit arguments in class field declarationsGravatar msozeau2008-01-02
* Better resolution of implicit parameters in typeclass binders, add extensiona...Gravatar msozeau2008-01-02
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Addition of more general tactics for equality. Functional extensionality and ...Gravatar msozeau2007-10-24
* Add more equality tactics. Upgrade program_simpl for discrimination of conjun...Gravatar msozeau2007-08-26
* A better Program documentation. Include it in the generated stdlib doc.Gravatar msozeau2007-08-08
* Move Program tactics into a proper theories/ directory as they are general pu...Gravatar msozeau2007-08-07