coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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-31
*	Added some tests to make more robust the tactique "Functional	courtieu	2003-03-01
*	Adding tests for the "functional induction" facility.	bertot	2003-02-27
*	The contribution of Pierre Courtieu on generating specialized induction schemes	bertot	2003-02-27