coq - The formal proof system

Age	Commit message (Expand)	Author
2003-10-16	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-15	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-14	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-13	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