aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/invfun.ml
AgeCommit message (Expand)Author
2006-02-17Julien:bertot
2006-02-17changed the decomposition of an induction schemecoq
2006-02-08Julien:bertot
2006-02-01New version of functional induction / inversion. By Julien Forest,coq