aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program/Equality.v
Commit message (Expand)AuthorAge
...
* Various fixes:Gravatar msozeau2008-05-15
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* 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
* 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