coq - The formal proof system

Age	Commit message (Expand)	Author
2006-09-16	Message modification in Function	jforest
2006-09-14	mise en conformite des messages d'erreur de Function avec la doc.	jforest
2006-09-01	Ajout possibilité clause "where" dans co-points fixes	herbelin
2006-08-25	two minor bug corrections in General Recursive Functions	jforest
2006-08-24	Amelioration 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-08-15	working on functional induction automation (tactic finduction and	courtieu
2006-08-11	Bug corrections in Function.	jforest
2006-08-08	In the old version, recursive functions cannot be declared inside a section	bertot
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-05	Use typing informations while defining graphs for Function.	jforest
2006-07-04	functional inversion now takes a quatified hypothesis as first argument	jforest
2006-07-04	adding comments and cleaning code	jforest
2006-07-04	- completely new version of "functional inversion" using inversion on	jforest
2006-06-29	forgot a file	jforest
2006-06-29	bug correction	jforest
2006-06-23	Passage des graphes de Function dans Type	jforest
2006-06-16	Ajout de tactiques expérimentales basée sur functional induction.	courtieu
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-06-12	changed comments.	courtieu
2006-06-07	functional induction can now be used with	jforest
2006-06-06	this time it's good	jforest
2006-06-06	Error in last commit	jforest
2006-06-06	protecting an uncaught exception Not_found	jforest
2006-06-06	+ ameliorating the tactic "functional induction"	jforest
2006-06-01	bug in alpha-conversion	jforest
2006-05-31	Replacing the old version of "functional induction" with the new one.	jforest
2006-05-30	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin
2006-05-29	small changes	jforest
2006-05-23	Error during last commit (coq didn't compile)	jforest
2006-05-23	Correcting a bug with ocaml <= 3.08.3 (Map.fold changing)	jforest
2006-05-22	LetTuple are now supported in Function	jforest
2006-05-07	+ correcting a bug in general recursive function (match e with _ => match f e...	jforest
2006-05-05	Correction in generate_graph (now handles fun _ => fix ....)	jforest
2006-05-03	Fixing two minor bugs in recdef and graph of function generation.	jforest
2006-05-03	Cleanning and factorizing code in funind. Spliting new_arg_principles into to...	jforest
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-04-27	- Distinction explicite des parties paramètres et arguments dans le type	herbelin
2006-04-27	Standardisation nom option_app en option_map	herbelin
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-12	Simplifying the proof of principles	jforest
2006-04-10	+ Changing a little functional schemes types	jforest
2006-03-20	Adding "New Functional Scheme"	jforest
2006-03-16	Cleaning dead code	jforest