aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/rawterm_to_relation.ml
AgeCommit message (Expand)Author
2006-05-22LetTuple are now supported in Functionjforest
2006-05-03Fixing two minor bugs in recdef and graph of function generation. jforest
2006-05-03Cleanning and factorizing code in funind. Spliting new_arg_principles into to...jforest
2006-04-27- Distinction explicite des parties paramètres et arguments dans le typeherbelin
2006-04-24+ Handling "if" and cast in GenFixpoint jforest
2006-04-10+ Changing a little functional schemes types jforest
2006-03-10cleaning 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-08Julien:bertot
2006-02-01New version of functional induction / inversion. By Julien Forest,coq