aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/indfun.ml
AgeCommit message (Expand)Author
2006-03-13Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.msozeau
2006-02-22Julien:bertot
2006-02-17Julien:bertot
2006-02-08One can use a measure {mes f x} instead of a well-founded relation in GenFixp...bertot
2006-02-08Julien:bertot
2006-02-01New version of functional induction / inversion. By Julien Forest,coq