aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/tacinvutils.mli
AgeCommit message (Expand)Author
2008-04-28menage dans funind + deplaceemnt de recdef dans funindjforest
2004-05-13"comments only" commit.coq
2004-02-09New version of Functional Scheme and functional induction. Deals withcoq
2003-03-31Correcting a bug occuring when the mimicked function had acourtieu
2003-02-27The contribution of Pierre Courtieu on generating specialized induction schemesbertot