coq - The formal proof system

Age	Commit message (Expand)	Author
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
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-12	maj	filliatr
2003-10-11	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	Logic_TypeSyntax disparu	herbelin
2003-10-11	Death of 'a somewhat cryptic module'	herbelin
2003-10-11	Death of 'a somewhat cryptic module'	herbelin
2003-10-11	mise a jour nouvelle syntaxe	barras
2003-10-10	maj	filliatr
2003-10-10	Suppression Grammar/Syntax	herbelin
2003-10-10	identity est equivalent sur Type (sauf sans argument)	herbelin
2003-10-10	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	Bug undo	herbelin
2003-10-10	Notation '^'	herbelin
2003-10-10	* empty log message *	herbelin
2003-10-10	Plus d'Eval Compute	herbelin
2003-10-10	MAJ commentaires	herbelin
2003-10-10	MAJ	herbelin