aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind/indfun_main.ml4
Commit message (Expand)AuthorAge
* Adding "New Functional Scheme" Gravatar jforest2006-03-20
* Cleaning dead code Gravatar jforest2006-03-16
* + Debugging and cleaning functional principle generation tacticGravatar jforest2006-03-14
* -Debugging multiple induction, a bug appeared when having functionGravatar courtieu2006-03-12
* Julien:Gravatar bertot2006-02-22
* Julien:Gravatar bertot2006-02-17
* One can use a measure {mes f x} instead of a well-founded relation in GenFixp...Gravatar bertot2006-02-08
* Julien:Gravatar bertot2006-02-08
* New version of functional induction / inversion. By Julien Forest,Gravatar coq2006-02-01