coq - The formal proof system

Age	Commit message (Expand)	Author
2003-04-07	Stratégie d'affichage des coercions plus défensive (mais pas très optimale)	herbelin
2003-04-07	Cosmetique	herbelin
2003-04-07	code mort	herbelin
2003-04-07	Espaces superflus	herbelin
2003-04-07	Renommage unicite/unicity pour la v8	herbelin
2003-04-07	Aérer les := et : de "assert"	herbelin
2003-04-07	Ajout cas Match	herbelin
2003-04-07	BEST redondant	herbelin
2003-04-07	Suppression des explicitations d'implicite inutiles	herbelin
2003-04-07	Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun implicite	herbelin
2003-04-07	Options d'affichage maintenant dans Constrextern	herbelin
2003-04-07	Options d'affichage maintenant dans Constrextern	herbelin
2003-04-04	maj	filliatr
2003-04-03	Documentation, généralisation à eq sur Type, preuves d'équivalence des	herbelin
2003-04-03	Backtrack du commit de Christine, qui posait probleme avec FTC	letouzey
2003-04-03	Légères simplifications code de Field; message d'erreur si pas égalité	herbelin
2003-04-03	maj	filliatr
2003-04-02	espace manquant	herbelin
2003-04-01	remplace == par = dans la tactique field pour que le debugger marche a nouvea...	narboux
2003-04-01	maj	filliatr
2003-04-01	Déplacement with_option dans Options	herbelin
2003-04-01	Correction bug #261 + amélioration nommage	herbelin
2003-04-01	Extension de Replace aux égalités entre preuves	herbelin
2003-04-01	Fail 1 pour traverser le match	herbelin
2003-04-01	maj	filliatr
2003-03-31	MAJ	herbelin
2003-03-31	Noms absolus	herbelin
2003-03-31	Ajout double_plus	herbelin
2003-03-31	Ajout Implicit Variable Type	herbelin
2003-03-31	Plus de eqT; message Fail	herbelin
2003-03-31	Ajout d'un message à FailTac	herbelin
2003-03-31	Ajout d'un message à FailTac; localisation des appels à des tactiques défi...	herbelin
2003-03-31	Mise en place d'un traducteur de noms v7->v8	herbelin
2003-03-31	Ajout d'un choix 'onlyparse'	herbelin
2003-03-31	Suppression des alias eqT/exT/exT2 en nouvelle syntaxe	herbelin
2003-03-31	Ajout VernacReserve et suppression des types re-inferables	herbelin
2003-03-31	Restauration de make_all_different (disparu depuis version 1.74) car sinon de...	herbelin
2003-03-31	Bug pattern_occ_hyp_list	herbelin
2003-03-31	Correcting a bug occuring when the mimicked function had a	courtieu
2003-03-31	Notation eqT superflue	herbelin
2003-03-31	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea
2003-03-31	minus a changé d'emplacement -> omega pas content	letouzey
2003-03-31	maj	filliatr
2003-03-29	eq fusionne avec eqT et devient par défaut sur Type,	herbelin
2003-03-29	indentation	herbelin
2003-03-29	Déplacement de minus dans Peano	herbelin
2003-03-29	Implicit Variables Type	herbelin
2003-03-29	Implicit Variables Type dans les inductive	herbelin
2003-03-29	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin
2003-03-29	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin