coq - The formal proof system

Age	Commit message (Expand)	Author
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
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-03-12	-Debugging multiple induction, a bug appeared when having function	courtieu
2006-03-10	cleaning	jforest
2006-03-07	Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain is_emp...	jforest
2006-02-22	Julien:	bertot
2006-02-17	Julien:	bertot
2006-02-17	changed the decomposition of an induction scheme	coq
2006-02-09	very minor bug correction and cleanning	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-03	added mli 's for the nex functional induction (forgotten last time).	coq
2006-02-01	New version of functional induction / inversion. By Julien Forest,	coq
2006-01-28	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin
2006-01-21	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin
2005-12-08	More exception handling in functional scheme.	coq
2005-12-02	Changement des named_context	gregoire
2005-09-16	changed the syntax categories of arguments of functional scheme	coq
2005-08-18	code cleaning. No changes as far as tested.	coq
2005-05-26	Correction of a bug in functional scheme. It raised with mutual	coq
2005-02-12	Uniformisation de destApplication en destApp	herbelin
2004-12-10	Hugo fixed a bug of refine, and it revealed a bug of functional	coq