coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Les records déclarés avec Record ne peuvent plus être récursifs (le	aspiwack	2009-01-19
*	DISCLAIMER	puech	2009-01-17
*	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau	2008-12-14
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	Suite commit 11539 sur notation Record dans (Co)Inductive (MAJ	herbelin	2008-11-05
*	Prise en compte des coercions dans les clauses "with" même si le type	herbelin	2008-04-23
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin	2007-08-27
*	New keyword "Inline" for Parameters and Axioms for automatic	soubiran	2007-04-25
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	Suite commit 9110 (uniformisation position notation dans les blocs inductifs)	herbelin	2006-09-01
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	removes several warnings in contrib/interface	bertot	2006-01-11
*	Achèvement suppression traducteur dans contrib/interface	herbelin	2005-12-26
*	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
*	make sure the implicit argument indications are in the right order	bertot	2004-03-03
*	Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...	herbelin	2004-01-13
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
*	Conjecture declare maintenant un axiome; reorganisation VernacDefinition	herbelin	2003-10-23
*	Mise en place possibilité de définitions locales dans les paramètres des i...	herbelin	2003-09-06
*	Ajout "at next level" dans Notation	herbelin	2003-04-17
*	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin	2003-04-09
*	* empty log message *	barras	2003-03-12
*	Ajout du traducteur	desmettr	2003-02-05
*	removes all references to ctast.ml the Makefile has been updated accordingly.	bertot	2003-01-22
*	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey	2002-12-03
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
*	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin	2002-10-28
*	Lazy manuelles dans le code	coq	2002-10-07
*	correcting the treatment of many tactics that use quant_hyp in file xlate.ml	bertot	2002-10-06
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour	herbelin	2002-07-11
*	Intgration uniforme de coercions dans les dclarations (Variable and co) et re...	herbelin	2002-06-03
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	compat ocaml 3.03	filliatr	2001-12-13
*	Renommage qualid_of_global en shortest_qualid_of_global	herbelin	2001-11-19
*	GROS COMMIT:	barras	2001-11-05
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin	2001-10-17
*	Transparent	barras	2001-09-20
*	Prsing	herbelin	2001-08-10
*	Pretty -> Prettyp	filliatr	2001-05-28
*	Files that handle the dialogue with the graphical user-interface pcoq.	bertot	2001-04-04