aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/invfun.ml
AgeCommit message (Expand)Author
2006-05-30Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...herbelin
2006-05-29small changes jforest
2006-03-12 -Debugging multiple induction, a bug appeared when having functioncourtieu
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