coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	maj	filliatr	2003-12-29
*	MAJ 8.0	herbelin	2003-12-28
*	Protection contre l'echec des tests parser pour la distrib	herbelin	2003-12-27
*	Suppression en v8	herbelin	2003-12-27
*	MAJ	herbelin	2003-12-27
*	Type le 'return' comme un type	herbelin	2003-12-27
*	maj	filliatr	2003-12-27
*	maj	filliatr	2003-12-26
*	maj	filliatr	2003-12-25
*	BUG	herbelin	2003-12-24
*	* empty log message *	barras	2003-12-24
*	Parenthesage du terme pour accepter 'of' comme non ident	herbelin	2003-12-24
*	* empty log message *	barras	2003-12-24
*	* empty log message *	barras	2003-12-24
*	Ajout delimiteur et arguments de scope pour list	herbelin	2003-12-24
*	Bug affichage Decompose	herbelin	2003-12-24
*	MAJ Notation	herbelin	2003-12-24
*	La correction precedente a mis en evidence un defaut de l'utilisation de intr...	herbelin	2003-12-24
*	changement de pose en set (pose n'etait pas utilise avec la semantique	barras	2003-12-24
*	maj	filliatr	2003-12-24
*	'of' restait par erreur mot-cle dans psyntax.ml4 en v8	herbelin	2003-12-23
*	Reparation semantique casse de Pose en v7	herbelin	2003-12-23
*	Reparation incompatibilites v7/v8 dans destruct; utilisation de noms t2_3 dan...	herbelin	2003-12-23
*	Retablissement de GIntuition juste pour FSets	herbelin	2003-12-23
*	Finalement, espacement autour du ':' pour a la fois exists, forall et fun	herbelin	2003-12-23
*	* empty log message *	barras	2003-12-23
*	Affichage opaque	herbelin	2003-12-23
*	Bug commit precedent	herbelin	2003-12-23
*	Renommages des hypotheses transformees car en raison des possibles dependance...	herbelin	2003-12-23
*	Changement numero magique; message d'erreur en cas de mauvaise syntaxe	herbelin	2003-12-23
*	maj	filliatr	2003-12-23
*	Mise en valeur intropattern de paires et acceptation dans le 'as' de inductio...	herbelin	2003-12-22
*	MAJ	herbelin	2003-12-22
*	maj	filliatr	2003-12-22
*	Affichage sur le modèle du forall pour le exists	herbelin	2003-12-21
*	Traduction PolyList/List dans la qualification	herbelin	2003-12-21
*	MAJ messages d'erreurs en accord avec la doc	herbelin	2003-12-20
*	Bug rattrapage erreur locate_reference	herbelin	2003-12-20
*	MAJ	herbelin	2003-12-20
*	maj	filliatr	2003-12-20
*	maj	filliatr	2003-12-20
*	Suppression de l'espace avant les notations commencant par un ident	herbelin	2003-12-19
*	Inductive Types : seuls les petits types sont unitaires	mohring	2003-12-19
*	Bug affichage des metas dans un environnement avec definitions locales (bug 277)	herbelin	2003-12-19
*	Substitution dans REvar; reparation bug 277	herbelin	2003-12-19
*	Substitution dans REvar et PEvar plutot que encodage via noeud application po...	herbelin	2003-12-19
*	Reset Initial uniquement interactivement	herbelin	2003-12-19
*	name_app accessible a tous dans Nameops	herbelin	2003-12-19
*	maj	filliatr	2003-12-19
*	maj	filliatr	2003-12-18