coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	In_dec transparent (wish #902)	herbelin	2004-12-19
*	Inutile de réserver les notations à base de '{ }'	herbelin	2004-12-06
*	MAJ changements ChoiceFacts	herbelin	2004-12-05
*	Paramétrisation du domaine des axiomes de choix + ajout description = choice...	herbelin	2004-12-05
*	compatibility with POWERPC	gregoire	2004-11-22
*	Généralisation à Type de certaines propriétés des relations	herbelin	2004-11-19
*	Copy of the definition of prodT (already in the standard library) removed.	sacerdot	2004-11-16
*	Changement dans les boxed values .	gregoire	2004-11-12
*	MAJ commentaire sur incohérence EM dans Set	herbelin	2004-11-07
*	Réponse à la conjecture que PI est indépendant de EM dans CC	herbelin	2004-11-02
*	COMMITED BYTECODE COMPILER	barras	2004-10-20