coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- 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-27
*	Replacing "GenFixpoint" with "Function" and "mes" with "measure"	jforest	2006-04-26
*	+ Handling "if" and cast in GenFixpoint	jforest	2006-04-24
*	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey	2006-04-14
*	Simplifying the proof of principles	jforest	2006-04-12
*	+ Changing a little functional schemes types	jforest	2006-04-10
*	Adding "New Functional Scheme"	jforest	2006-03-20
*	Cleaning dead code	jforest	2006-03-16
*	+ Debugging and cleaning functional principle generation tactic	jforest	2006-03-14
*	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau	2006-03-13
*	-Debugging multiple induction, a bug appeared when having function	courtieu	2006-03-12
*	cleaning	jforest	2006-03-10
*	Coq did not compile in Ocaml 3.06 and 3.07 since Map.S did not contain is_emp...	jforest	2006-03-07
*	Julien:	bertot	2006-02-22
*	Julien:	bertot	2006-02-17
*	changed the decomposition of an induction scheme	coq	2006-02-17
*	very minor bug correction and cleanning	bertot	2006-02-09
*	One can use a measure {mes f x} instead of a well-founded relation in GenFixp...	bertot	2006-02-08
*	Julien:	bertot	2006-02-08
*	added mli 's for the nex functional induction (forgotten last time).	coq	2006-02-03
*	New version of functional induction / inversion. By Julien Forest,	coq	2006-02-01
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin	2005-12-26
*	More exception handling in functional scheme.	coq	2005-12-08
*	Changement des named_context	gregoire	2005-12-02
*	changed the syntax categories of arguments of functional scheme	coq	2005-09-16
*	code cleaning. No changes as far as tested.	coq	2005-08-18
*	Correction of a bug in functional scheme. It raised with mutual	coq	2005-05-26
*	Uniformisation de destApplication en destApp	herbelin	2005-02-12
*	Hugo fixed a bug of refine, and it revealed a bug of functional	coq	2004-12-10
*	Code mort	herbelin	2004-12-06
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1	herbelin	2004-08-24
*	"comments only" commit.	coq	2004-05-13
*	Correction of a bug in Functional Scheme discovered when porting the	coq	2004-02-10
*	New version of Functional Scheme and functional induction. Deals with	coq	2004-02-09
*	Obsolete, cf Funind.v dans test-suite	herbelin	2003-11-29
*	Retour des _eq en v8	herbelin	2003-11-27
*	petits changements de syntaxe	barras	2003-11-12
*	Compatibilite V7 des noms d'hypotheses	herbelin	2003-10-07
*	Cacher les .v8	herbelin	2003-10-03
*	Plus de nom commencant par '_' en V8	herbelin	2003-10-02
*	Simplification vis a vis de Declare	herbelin	2003-09-12
*	Typo	herbelin	2003-06-10
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Ajout d'un message à FailTac	herbelin	2003-03-31