aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/new_arg_principle.ml
AgeCommit message (Expand)Author
2006-05-03Cleanning and factorizing code in funind. Spliting new_arg_principles into to...jforest
2006-04-24+ Handling "if" and cast in GenFixpoint jforest
2006-04-12Simplifying the proof of principlesjforest
2006-04-10+ Changing a little functional schemes types jforest
2006-03-20Adding "New Functional Scheme" jforest
2006-03-14+ Debugging and cleaning functional principle generation tacticjforest
2006-02-22Julien:bertot
2006-02-17Julien:bertot
2006-02-09very minor bug correction and cleanningbertot
2006-02-08Julien:bertot
2006-02-01New version of functional induction / inversion. By Julien Forest,coq