aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/tacinv.ml4
AgeCommit message (Expand)Author
2003-10-07Compatibilite V7 des noms d'hypothesesherbelin
2003-10-02Plus de nom commencant par '_' en V8herbelin
2003-03-31Ajout d'un message à FailTacherbelin
2003-03-31Correcting a bug occuring when the mimicked function had acourtieu
2003-03-01Added some tests to make more robust the tactique "Functionalcourtieu
2003-02-27The contribution of Pierre Courtieu on generating specialized induction schemesbertot