coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau	2006-03-22
*	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin	2006-03-22
*	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau	2006-03-13
*	Julien:	bertot	2006-02-08
*	New version of functional induction / inversion. By Julien Forest,	coq	2006-02-01
*	maj	coq	2005-12-30
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin	2005-12-26
*	maj	coq	2005-11-18
*	Modifications in the .depend files for the contrib/recdef directory	bertot	2005-11-07
*	new congruence	corbinea	2005-08-17
*	Subtac: traitement correct des existentielles et de la rÃ©cursion.	coq	2005-07-15
*	reflexive tauto	corbinea	2005-07-15
*	Added subtac contrib.	coq	2005-05-25
*	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot	2005-05-20
*	tactiques prouveurs premier ordre dans contrib/dp/	coq	2005-03-16
*	Ajout g_xml.ml4 et cic2Xml.ml	herbelin	2005-02-04
*	maj	filliatr	2004-08-26
*	maj	filliatr	2004-07-29
*	MAJ	herbelin	2004-07-16
*	maj	filliatr	2004-05-04
*	maj	filliatr	2004-01-28
*	maj	filliatr	2004-01-15
*	Ground update + Linear removal	corbinea	2003-10-16
*	suppression de newtauto	corbinea	2003-07-02
*	Ground major update ... mmm, sounds exciting !	corbinea	2003-06-15
*	moved engine.ml4 to ground.ml4, added option 'Ground Depth'	corbinea	2003-05-26
*	Added the Ground tactic.	corbinea	2003-04-25
*	* Ajout du traducteur nouvelle syntaxe *	barras	2003-03-12
*	maj	filliatr	2003-02-28
*	The contribution of Pierre Courtieu on generating specialized induction schemes	bertot	2003-02-27
*	Bringing Linear back to life (Still somewhat buggy).	corbinea	2003-02-24
*	Ajout de LinearIntuition; Ajout de New(Tauto\|Intuition\|LinearIntuition).	corbinea	2003-01-23
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	Adding the congruence closure tactics (CC and CCsolve).	corbinea	2002-10-01
*	maj	filliatr	2002-09-20
*	maj	filliatr	2002-09-20
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	extraction vers scheme	letouzey	2002-06-07
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	contrib/interface/dad.ml4 had no real need of streams, it should have been	bertot	2001-12-19
*	reparation du make depend et du .depend	letouzey	2001-12-19
*	Les réduction dans les hypothèses s'appliquent maintenant au corps de la d�...	herbelin	2001-06-25
*	Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compil...	herbelin	2001-06-25
*	Ajout de Field	delahaye	2001-04-19
*	réparation Correctness; options Extraction (changement de syntaxe)	filliatr	2001-04-10
*	Ajout lemmes arithmetiques	mohring	2001-04-08
*	branchement extraction (bytecode seulement)	filliatr	2001-03-30
*	simplification du make depend; fonctions de stat. util. memoire dans certains...	filliatr	2001-02-08