coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	A bit of cleaning around name generation + creation of dedicated file namegen.ml	herbelin	2009-11-09
*	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
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	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
*	Déplacement traducteur de nom dans Constrextern pour accès aux noms longs	herbelin	2003-06-10
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	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
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	reparation de Locate	barras	2001-11-29
*	nouvel algo de conversion plus uniforme	barras	2001-11-29
*	GROS COMMIT:	barras	2001-11-05