coq - The formal proof system

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