coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre)	herbelin	2003-10-04
*	NEWVO doit apparaitre apres VO + divers	herbelin	2003-10-04
*	maj	filliatr	2003-10-04
*	pr_vernac est paresseux; States.unfreeze seulement après que msgnl ait	herbelin	2003-10-03
*	Bug cible newtheories/Init + divers	herbelin	2003-10-03
*	Cacher les .v8	herbelin	2003-10-03
*	Correction bug explosion de la taille de la liste loaded_modules	herbelin	2003-10-03
*	Nettoyage, simplification et compatibilite -j	herbelin	2003-10-03
*	oubli de deux flags -v7	letouzey	2003-10-03
*	* empty log message *	barras	2003-10-03
*	Pas de renommage des noms de section	herbelin	2003-10-02
*	as au niveau de app	herbelin	2003-10-02
*	Hypothesis mot-cle	herbelin	2003-10-02
*	Traduction des tests success et test en v8	herbelin	2003-10-02
*	Plus de nom commencant par '_' en V8	herbelin	2003-10-02
*	Le nom '_' n'est plus valable en v8 pour nommer les variables	herbelin	2003-10-02
*	Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...	herbelin	2003-10-01
*	cosmetique	herbelin	2003-10-01
*	Implantation de l'option 'format' des Notations	herbelin	2003-10-01
*	maj	filliatr	2003-10-01
*	'_ = _ = _' maintenant predefini, meme en V7	herbelin	2003-09-30
*	Ajout 'Close Scope', mise en place de la structure pour un modificateur 'format'	herbelin	2003-09-30
*	Les notations hors scope s'empilent maintenant comme des scopes ne	herbelin	2003-09-30
*	code mort	herbelin	2003-09-30
*	Les notations hors scope s'empilent maintenant comme des scopes ne	herbelin	2003-09-30
*	Ajout 'Close Scope'.	herbelin	2003-09-30
*	Ajout 'Close Scope'.	herbelin	2003-09-30
*	Ajout 'Close Scope'.	herbelin	2003-09-30
*	Oubli du type du terme a filtrer quand pas d'argument dans la traduction de case	herbelin	2003-09-29
*	Prise en compte d'un inductif sans argument dans le 'in' des 'match'	herbelin	2003-09-29
*	oups	letouzey	2003-09-28
*	2 pbs de plus réglés concernant Setoid Ring:	letouzey	2003-09-28
*	une induction de moins dans lt_eq_lt_dec	letouzey	2003-09-28
*	well_founded_induction de nouveau transparent	letouzey	2003-09-28
*	maj	filliatr	2003-09-27
*	Bug about	herbelin	2003-09-26
*	Syntaxe plus liberale pour le type des arguments de filtrage du 'match'	herbelin	2003-09-26
*	Syntaxe plus liberale pour le type des arguments de filtrage du 'match'; trad...	herbelin	2003-09-26
*	MAJ	herbelin	2003-09-26
*	pa_ifdef.cmo redondant	herbelin	2003-09-26
*	Ajout now_show	herbelin	2003-09-26
*	About, Infix	herbelin	2003-09-26
*	'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...	herbelin	2003-09-26
*	Ajout 'About'	herbelin	2003-09-26
*	Induction -> NewInduction; '++' pour app	herbelin	2003-09-26
*	Nouvelle serie de traductions	herbelin	2003-09-26
*	Re-possibilite changement chaine infixe en passant v7 a v8	herbelin	2003-09-26
*	Passage de Destruct a NewDestruct; '-' pour negb	herbelin	2003-09-26
*	Structuration de fast_integer en operations sur positive, proprietes des oper...	herbelin	2003-09-26
*	Un peu plus de souplesse dans la globalisation des noms utilises par les tact...	herbelin	2003-09-26