coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Commentaires	herbelin	2003-10-23
*	Documentation/Structuration	herbelin	2003-10-22
*	Documentation/Structuration	herbelin	2003-10-22
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
*	Redondance de dec_eq_nat	herbelin	2003-10-21
*	Type relation dans Datatypes	herbelin	2003-10-21
*	Maintenant avant Datatypes	herbelin	2003-10-21
*	ajouts	herbelin	2003-10-21
*	R passe dans Set !	herbelin	2003-10-20
*	20 est uniquement associatif a gauche	herbelin	2003-10-17
*	Des implicites plus 'naturels' pour eq_ind, identity_ind and co	herbelin	2003-10-17
*	nouvelle syntaxe de ltac	barras	2003-10-16
*	lettac -> set	barras	2003-10-16
*	Syntax error	herbelin	2003-10-16
*	Suppression des surcharge de regles de grammaire en v7	herbelin	2003-10-16
*	Pour eviter des regles redondantes en v7	herbelin	2003-10-16
*	FTC_P2 maintenant dans RIneq	herbelin	2003-10-16
*	Ajout de quelques lemmes cles	herbelin	2003-10-16
*	Affichage = au lieu de == en v7	herbelin	2003-10-15
*	Nettoyage argument de nil	herbelin	2003-10-15
*	Changement 'as notation' en 'where notation'	herbelin	2003-10-14
*	Argument de except, error implicite seulement en v8; Changement 'as notation'...	herbelin	2003-10-14
*	Argument de None implicite seulement en v8	herbelin	2003-10-14
*	Argument implicite pour None, error, except	herbelin	2003-10-13
*	Notations pour l'exponentiation	herbelin	2003-10-13
*	Enregistrement '^' en v8	herbelin	2003-10-13
*	mise a jour nouvelle syntaxe	barras	2003-10-11
*	nat_scope ouvert par defaut	herbelin	2003-10-10
*	identity est equivalent sur Type (sauf sans argument)	herbelin	2003-10-10
*	type_scope	herbelin	2003-10-10
*	Suppression de definitions equivalentes	herbelin	2003-10-10
*	Notation '^'	herbelin	2003-10-10
*	Plus d'Eval Compute	herbelin	2003-10-10
*	MAJ commentaires	herbelin	2003-10-10
*	Delimiters N devient 'nat'	herbelin	2003-10-10
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Renommage en v8 de PolyList en List et List en MonoList	herbelin	2003-10-10
*	Renommage en v8 de PolyList en List et List en MonoList	herbelin	2003-10-10
*	Cacher les .v8	herbelin	2003-10-03
*	Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...	herbelin	2003-10-01
*	'_ = _ = _' maintenant predefini, meme en V7	herbelin	2003-09-30
*	une induction de moins dans lt_eq_lt_dec	letouzey	2003-09-28
*	well_founded_induction de nouveau transparent	letouzey	2003-09-28
*	'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...	herbelin	2003-09-26
*	Induction -> NewInduction; '++' pour app	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
*	add_x_x de fast_integer vers auxiliary	herbelin	2003-09-25
*	Retour provisoire a une section	herbelin	2003-09-25
*	Suppression section, ce qui evite de repliquer les declarations d'Infix	herbelin	2003-09-24