coq - The formal proof system

Age	Commit message (Expand)	Author
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
2004-12-06	Code mort	herbelin
2004-11-16	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-08-24	Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1	herbelin
2004-05-13	"comments only" commit.	coq
2004-02-10	Correction of a bug in Functional Scheme discovered when porting the	coq
2004-02-09	New version of Functional Scheme and functional induction. Deals with	coq
2003-11-29	Obsolete, cf Funind.v dans test-suite	herbelin
2003-11-27	Retour des _eq en v8	herbelin
2003-11-12	petits changements de syntaxe	barras
2003-10-07	Compatibilite V7 des noms d'hypotheses	herbelin
2003-10-03	Cacher les .v8	herbelin
2003-10-02	Plus de nom commencant par '_' en V8	herbelin
2003-09-12	Simplification vis a vis de Declare	herbelin
2003-06-10	Typo	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-03-31	Ajout d'un message à FailTac	herbelin
2003-03-31	Correcting a bug occuring when the mimicked function had a	courtieu
2003-03-31	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea
2003-03-01	Added some tests to make more robust the tactique "Functional	courtieu
2003-02-27	Adding tests for the "functional induction" facility.	bertot
2003-02-27	The contribution of Pierre Courtieu on generating specialized induction schemes	bertot