coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
*	Alignement du comportement des implicites d'inductif en sortie de section sur...	herbelin	2003-04-09
*	Renommage K; equivalence JMeq et eq_dep sur Type	herbelin	2003-04-09
*	Defined	herbelin	2003-04-09
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".	herbelin	2003-04-09
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
*	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin	2003-04-09
*	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin	2003-04-09
*	Prise en compte affichage coercions traducteur dans Constrextern	herbelin	2003-04-09
*	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-08
*	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-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