aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/indfun_main.ml4
AgeCommit message (Expand)Author
2006-04-26Replacing "GenFixpoint" with "Function" and "mes" with "measure"jforest
2006-04-10+ Changing a little functional schemes types jforest
2006-03-20Adding "New Functional Scheme" jforest
2006-03-16Cleaning dead code jforest
2006-03-14+ Debugging and cleaning functional principle generation tacticjforest
2006-03-12 -Debugging multiple induction, a bug appeared when having functioncourtieu
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