coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Cosmetique	herbelin	2003-04-14
*	Localisation des appels de tactiques définies sans arguments	herbelin	2003-04-14
*	Bug: lookup inapproprie dans subst_tactic	herbelin	2003-04-14
*	Correction bug PR#278	coq	2003-04-14
*	Local 'o'	herbelin	2003-04-14
*	Open Scope en Local	herbelin	2003-04-12
*	Ajout option 'Local' à Infix et Notation	herbelin	2003-04-11
*	Ajout option 'Local' à Infix et Notation	herbelin	2003-04-11
*	Explicitation arguments de eq	herbelin	2003-04-11
*	Affichage des inductifs	herbelin	2003-04-10
*	Open Scope remplace Import	herbelin	2003-04-10
*	Calcul automatique de l'implicite de nil pour que l'affichage sache le traiter	herbelin	2003-04-10
*	Affichage forcé des implicites contextuels si pas de contexte connu	herbelin	2003-04-10
*	Remplacement Import par Open Scope en v8	herbelin	2003-04-10
*	Suppression de quelques espaces superflus	herbelin	2003-04-10
*	Relachement globalisation Unfold en usage interactif	herbelin	2003-04-10
*	coqide: undo fix	monate	2003-04-10
*	* empty log message *	monate	2003-04-10
*	* empty log message *	monate	2003-04-10
*	coqide: bug highlight corrige	monate	2003-04-10
*	coqide: completion support	monate	2003-04-10
*	set_focus	marche	2003-04-10
*	coqide: thread bug fix	monate	2003-04-10
*	Trop de restriction pour les TacDef	herbelin	2003-04-10
*	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