coq - The formal proof system

Age	Commit message (Expand)	Author
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-09	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-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