coq - The formal proof system

Age	Commit message (Expand)	Author
2003-04-09	Prise en compte affichage coercions traducteur dans Constrextern	herbelin
2003-04-08	on repasse aussi -thread a Caml	filliatr
2003-04-08	test: un boolean et une fonction check_for_interrupt inseree dans la conversi...	filliatr
2003-04-08	Prise en compte des variables de grammaires de tactiques et dédollarisation ...	herbelin
2003-04-08	Application de l'absence d'export aux modules	herbelin
2003-04-08	En-tete doc	herbelin
2003-04-08	Ajout option "Local" à "Open Scope"	herbelin
2003-04-08	maj	filliatr
2003-04-07	Affichage des tactiques en v8	herbelin
2003-04-07	lconstr pour genterm en v8	herbelin
2003-04-07	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-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