aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/rawtermops.ml
AgeCommit message (Expand)Author
2006-06-06+ ameliorating the tactic "functional induction"jforest
2006-06-01bug in alpha-conversionjforest
2006-05-22LetTuple are now supported in Functionjforest
2006-04-27Standardisation nom option_app en option_mapherbelin
2006-04-24+ Handling "if" and cast in GenFixpoint jforest
2006-04-10+ Changing a little functional schemes types jforest
2006-03-07Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain is_emp...jforest
2006-02-17Julien:bertot
2006-02-01New version of functional induction / inversion. By Julien Forest,coq