coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Deplacement pr_subgoal and co vers Pfedit	herbelin	2003-10-13
*	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin	2003-10-13
*	Protection contre les noms de lemmes existant deja	herbelin	2003-10-13
*	Deplacement pr_subgoal and co vers Pfedit; Ajout SearchNamed	herbelin	2003-10-13
*	Deplacement next_global_ident_away dans Termops	herbelin	2003-10-13
*	maj	filliatr	2003-10-12
*	reparation Undo suite	herbelin	2003-10-11
*	Uniformisation comportement decompEq pour corriger un bug introduit dans le I...	herbelin	2003-10-11
*	Bug calcul du nom de la premiere equation	herbelin	2003-10-11
*	translate_file etait abusivement positionne	herbelin	2003-10-11
*	Ajout fnl() dans About	herbelin	2003-10-11