aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind/rawterm_to_relation.ml
AgeCommit message (Expand)Author
2006-09-27Detection des paramettres pour les Functions bien fondeesjforest
2006-09-01Ajout possibilité clause "where" dans co-points fixes herbelin
2006-08-24Amelioration des messages d'erreur de Fucntion jforest
2006-08-16+ timide essai pour le traitement des as dans les patterns lors de la generat...jforest
2006-07-18Code cleaning in Functionjforest
2006-07-10+functional inversion now takes the function to invert as an optional argument. jforest
2006-07-05Use typing informations while defining graphs for Function. jforest
2006-07-04adding comments and cleaning code jforest
2006-07-04- completely new version of "functional inversion" using inversion onjforest
2006-06-23Passage des graphes de Function dans Type jforest
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