coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	maj	filliatr	2003-04-10
*	cast de nil	herbelin	2003-04-09
*	Affichage des inductifs	herbelin	2003-04-09
*	nil en implicite dans la v8	herbelin	2003-04-09
*	Bug init_function	herbelin	2003-04-09
*	Synchronisation séparée des implicites pour l'affichage du traducteur;	herbelin	2003-04-09
*	Formattage affichage	herbelin	2003-04-09
*	Correction Show Implicits	herbelin	2003-04-09
*	Ajout Open Scope	herbelin	2003-04-09
*	Mécanisme plus simple et efficace pour traduire les implicites	herbelin	2003-04-09
*	Gestion synchronisation des Impargs.*_out et des Impargs._strict dans Impargs	herbelin	2003-04-09
*	Coqide : introduction des coprocessus. CoqIde est maintenant interruptible	monate	2003-04-09
*	Activation des implicites pour la v8	herbelin	2003-04-09
*	MAJ	herbelin	2003-04-09
*	Bugs synchronisation pour gestion traduction des implicites	herbelin	2003-04-09
*	Synchronisation avec reset	herbelin	2003-04-09
*	Ajout option -v8 à coqtopnew pour permettre le changement de comportement de...	herbelin	2003-04-09
*	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