coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	lettac -> set	barras	2003-10-16
*	Marge presqu'a 80, maximum indentation a 50 pour une meilleure lisibilite	herbelin	2003-10-16
*	* empty log message *	barras	2003-10-16
*	oups! ca compile maintenant	barras	2003-10-16
*	translator avoids printing a . followed by a ( by inserting a space	barras	2003-10-16
*	Ground update + Linear removal	corbinea	2003-10-16
*	Syntax error	herbelin	2003-10-16
*	Message d'erreur	herbelin	2003-10-16
*	Debranchement de l'affichage systematique des projections avec la notation po...	herbelin	2003-10-16
*	Suppression des surcharge de regles de grammaire en v7	herbelin	2003-10-16
*	Debranchement de l'affichage systematique des projections avec la notation po...	herbelin	2003-10-16
*	Branchement sur RIneq	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
*	Bug Search	herbelin	2003-10-16
*	Mise en conformite return_type en fonction de la doc	herbelin	2003-10-15
*	Affichage = au lieu de == en v7	herbelin	2003-10-15
*	Gestion encore plus affinee des implicites	herbelin	2003-10-15
*	Pour eviter que newtheories/Lists/List.v soit refait quand PolyList.v est ref...	herbelin	2003-10-15
*	Nettoyage argument de nil	herbelin	2003-10-15
*	maj	filliatr	2003-10-14
*	Gestion affinee des implicites	herbelin	2003-10-14
*	Nouvelles traductions de noms; mot-cle; affichage implicites par le traducteur	herbelin	2003-10-14
*	En v7 sans traducteur, une incoherence virtuelle de syntaxe V8 n'est pas une ...	herbelin	2003-10-14
*	Test obsolete	herbelin	2003-10-14
*	identityT = identity	herbelin	2003-10-14
*	Changement 'as notation' en 'where notation'	herbelin	2003-10-14
*	Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...	herbelin	2003-10-14
*	Changement 'as notation' en 'where notation'; protection 'nat_scope'; afficha...	herbelin	2003-10-14
*	Changement 'as notation' en 'where notation'; Plus d'uniformite dans la gesti...	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
*	maj	filliatr	2003-10-13
*	Ajout projections de triplet	herbelin	2003-10-13
*	Admitted rendu independant de Conjecture: plus pratique en mode interactif	herbelin	2003-10-13
*	Ground update changing left-arrow-arrow rule.	corbinea	2003-10-13
*	Export is_section_variable	herbelin	2003-10-13
*	Bug introduit dans start_proof par le commit precedent	herbelin	2003-10-13
*	Argument implicite pour None, error, except	herbelin	2003-10-13
*	MAJ	herbelin	2003-10-13
*	Notations pour l'exponentiation	herbelin	2003-10-13
*	Enregistrement '^' en v8	herbelin	2003-10-13
*	Cleaning	herbelin	2003-10-13
*	Ameliration affichage inductifs	herbelin	2003-10-13
*	Un Try supplementaire utile pour la compatibilite, car bring_hyps dans genera...	herbelin	2003-10-13
*	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin	2003-10-13
*	Petits bugs	herbelin	2003-10-13
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
*	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin	2003-10-13