aboutsummaryrefslogtreecommitdiff
path: root/contrib/rtauto
AgeCommit message (Expand)Author
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-03-14Makefile: ml dependencies of contribs are moved to .mllib filesletouzey
2008-12-16Take advantage of natdynlink when available: almost all contribs become loada...letouzey
2008-03-16Reorganize Program and Classes theories. Requiring Setoid no longer setsmsozeau
2008-03-06Plug the new setoid implemtation in, leaving the original one commentedmsozeau
2008-01-29Correction du bug #1785notin
2006-12-28Remplacement de la définition de Pind et Prec par une définitionherbelin
2006-09-20Declarative Proof Language: main commitcorbinea
2006-05-31Replacing the old version of "functional induction" with the new one. jforest
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...herbelin
2005-12-02Changement des named_contextgregoire
2005-08-17new congruencecorbinea
2005-07-15reflexive tautocorbinea