coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Fix premature optimisation in dependent induction: even variable args need	msozeau	2009-04-10
*	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin	2006-12-12
*	Ajout combinateurs option_fold_left et name_fold_map	herbelin	2006-10-09
*	Changement anomaly en failwith dans out_name pour utilisation par map_succeed	herbelin	2006-04-24
*	Prise en compte dans cut_ident des idents de la form _23 qui sont officiellem...	herbelin	2004-10-12
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	Nouvelle en-tête	herbelin	2004-07-16
*	name_app accessible a tous dans Nameops	herbelin	2003-12-19
*	Fonctions utiles	herbelin	2003-09-23
*	error	herbelin	2003-09-09
*	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin	2003-06-10
*	Extension renommage	herbelin	2003-05-20
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Deplacement lemmes sur fact de Reals vers Arith	herbelin	2003-05-14
*	Orthographe anglaise - typos	herbelin	2003-05-13
*	Orthographe anglaise	herbelin	2003-05-13
*	En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...	herbelin	2003-04-29
*	Renommage unicite/unicity pour la v8	herbelin	2003-04-07
*	Mise en place d'un traducteur de noms v7->v8	herbelin	2003-03-31
*	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin	2003-03-29
*	Petit netoyage dans lib	coq	2002-12-19
*	Corrections de gestion des univers et modules + meilleure gestions des noms...	coq	2002-12-09
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	compat ocaml 3.03	filliatr	2001-12-13
*	reparation de Locate	barras	2001-11-29
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	GROS COMMIT:	barras	2001-11-05