coq - The formal proof system

Age	Commit message (Expand)	Author
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
2003-10-10	Typo	herbelin
2003-10-10	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin
2003-10-10	Delimiters N devient 'nat'	herbelin
2003-10-10	Cablage en dur de inversion	herbelin
2003-10-10	code mort	herbelin
2003-10-10	show_subgoals dans Pfedit	herbelin
2003-10-10	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin
2003-10-10	MAJ .v8	herbelin
2003-10-10	pf_get_new_id en provenance de feu wcclausenv	herbelin
2003-10-10	Suppression clenv_change_head que seul Wcclausenv utisait	herbelin
2003-10-10	Dead of 'a somewhat cryptic module'	herbelin
2003-10-10	Dead of 'a somewhat cryptic module' (Inv doesn't use applyUsing any longer; p...	herbelin
2003-10-10	Ajout printers pour constr et constr_pattern (sans traduction)	herbelin
2003-10-10	Unification lemInv et lemInv_in	herbelin
2003-10-10	pr_tactic sans traduction; affichage Inversion	herbelin
2003-10-10	Cablage en dur de inversion	herbelin
2003-10-10	Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'	herbelin
2003-10-10	Intégration de la premiere partie de 'hightactics' dans 'tactics' suite à c...	herbelin
2003-10-10	Affichage des buts par Pfedit pour utilisation par les tactiques	herbelin
2003-10-10	Affichage des buts par Pfedit pour utilisation par les tactiques (Setoid_repl...	herbelin
2003-10-10	Gestion en temps constant de la pile des Unfo; affichage des buts par Pfedit ...	herbelin
2003-10-10	Gestion en temps constant de la pile des Unfo	herbelin