coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Modularisation des preuves concernant la logique classique, l'indiscernabilit...	herbelin	2006-03-05
*	Commentaires	herbelin	2006-03-05
*	Renommage du IP classique pour éviter confusion avec IP constructif	herbelin	2006-03-05
*	Ajout étude IP généralisé, Gödel-Dummett, buveur	herbelin	2006-03-05
*	Petite simplification en passant	herbelin	2006-03-04
*	Titres moins envahissants pour coqdoc	herbelin	2006-03-04
*	quelques raccourcis commodes + un f_equal plus efficace	letouzey	2006-02-27
*	Ajout 'exists! x:A, P (suite)	herbelin	2006-02-23
*	Ajout 'exists! x:A, P	herbelin	2006-02-23
*	Minimum pour documentation TeX de la biblio	herbelin	2006-02-22
*	MAJ	herbelin	2006-02-22
*	Bug Scope	herbelin	2006-02-12
*	Nettoyage Zmin.v, création Zmax.v et Zminmax.v	herbelin	2006-02-12
*	Nettoyage Bool:	herbelin	2006-02-12
*	Unification max_case et max_case2	herbelin	2006-02-12
*	Unification min_case et min_case2	herbelin	2006-02-12
*	Commentaires et compatibilité coqdoc	herbelin	2006-02-11
*	code mort	herbelin	2006-02-10
*	Ajout bibliothèque String de Laurent Théry	herbelin	2006-02-08
*	Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru...	herbelin	2006-02-06
*	Ajout décidabilité	herbelin	2006-01-31
*	Application de la suggestion de Nicolas Magaud (#1060)	herbelin	2006-01-22
*	Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind es...	herbelin	2006-01-21
*	Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Acc	herbelin	2006-01-21
*	Correction associativité de IF et exists (visible à l'affichage uniquement ...	herbelin	2006-01-19
*	Application du souhait de transparence de well_founded_ltof (#1007)	herbelin	2005-12-30
*	Contrepartie de la suppression des boites automatiques dans format	herbelin	2005-12-22
*	changement parametres inductifs dans les theories	mohring	2005-11-30
*	* empty log message *	letouzey	2005-08-26
*	Fix sumbool_not hint (on behalf of cpaulin).	coq	2005-07-15
*	add a left and right tactic for classical logic	narboux	2005-07-15
*	Détection d'un Fold incorrect suite à correction bug #986	herbelin	2005-07-13
*	Détection d'un Fold incorrect suite à correction bug #986	herbelin	2005-07-13
*	Documentation	herbelin	2005-05-19
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Finalement, préservation de la compatibilité pour Z_lt_induction et ajout p...	herbelin	2005-05-02
*	Lemme de passage de l'autre côté d'une égalité	herbelin	2005-05-02
*	Fixed hypotheses of Z_lt_induction (see #957)	herbelin	2005-04-26
*	Added option_map	herbelin	2005-03-31
*	Missing translating a 'O' into a '0' (again - cf bug #947); removed useless h...	herbelin	2005-03-29
*	Missing translating a 'O' into a '0' (again)	herbelin	2005-03-29
*	Missing translating a 'O' into a '0'	herbelin	2005-03-24
*	MAJ PolyList -> List	herbelin	2005-03-16
*	quelques tactics ltac	letouzey	2005-02-23
*	Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des jours...	coq	2005-02-07
*	Suppression de l'Unboxed des opérations sur positive (cf bug 898)	herbelin	2005-02-04
*	Essai d'utilisation de 'where' pour les notations	herbelin	2005-02-04
*	Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs	herbelin	2005-02-03
*	legere simplification des preuves de le_S_n et pred_le	letouzey	2005-02-03
*	Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs	herbelin	2005-02-03