coq - The formal proof system

Age	Commit message (Expand)	Author
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-09-27	Detection des paramettres pour les Functions bien fondees	jforest
2006-09-19	Gestion des arguments implicites dans les Functions bien fondees	jforest
2006-09-18	correction of bug #1220	jforest
2006-09-14	mise en conformite des messages d'erreur de Function avec la doc.	jforest
2006-08-24	Amelioration des messages d'erreur de Fucntion	jforest
2006-08-11	Bug corrections in Function.	jforest
2006-07-18	Code cleaning in Function	jforest
2006-07-18	Code cleaning in Function	jforest
2006-07-13	bug correction when defining graph of fixpoints/definitions not generated by ...	jforest
2006-07-10	+functional inversion now takes the function to invert as an optional argument.	jforest
2006-07-04	- completely new version of "functional inversion" using inversion on	jforest
2006-06-13	ajout d'un argument with_clean a Indfun.functional_induction permettant de ch...	jforest
2006-06-13	rearrangement du code: deplacement du code effectuant functional	courtieu
2006-05-22	LetTuple are now supported in Function	jforest
2006-05-05	Correction in generate_graph (now handles fun _ => fix ....)	jforest
2006-05-03	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest
2006-04-26	Replacing "GenFixpoint" with "Function" and "mes" with "measure"	jforest
2006-04-24	+ Handling "if" and cast in GenFixpoint	jforest
2006-04-14	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey
2006-04-10	+ Changing a little functional schemes types	jforest
2006-03-20	Adding "New Functional Scheme"	jforest
2006-03-14	+ Debugging and cleaning functional principle generation tactic	jforest
2006-03-13	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau
2006-02-22	Julien:	bertot
2006-02-17	Julien:	bertot
2006-02-08	One can use a measure {mes f x} instead of a well-founded relation in GenFixp...	bertot
2006-02-08	Julien:	bertot
2006-02-01	New version of functional induction / inversion. By Julien Forest,	coq