coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Ajout translate	herbelin	2003-04-07
*	Typo	herbelin	2003-04-07
*	Nommage explicite des hypotheses introduites quand le nom existe aussi comme ...	herbelin	2003-04-07
*	Globalisation tactiques	herbelin	2003-04-07
*	Mauvaise resolution conflit dans commit precedent	herbelin	2003-04-07
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	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-07
*	maj	filliatr	2003-04-04
*	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-03
*	espace manquant	herbelin	2003-04-02
*	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-04-01
*	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-31