coq - The formal proof system

Age	Commit message (Expand)	Author
2006-02-08	Ajout bibliothèque String de Laurent Théry	herbelin
2006-02-06	Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru...	herbelin
2006-01-31	Ajout décidabilité	herbelin
2006-01-22	Application de la suggestion de Nicolas Magaud (#1060)	herbelin
2006-01-21	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-19	Correction associativité de IF et exists (visible à l'affichage uniquement ...	herbelin
2005-12-30	Application du souhait de transparence de well_founded_ltof (#1007)	herbelin
2005-12-22	Contrepartie de la suppression des boites automatiques dans format	herbelin
2005-11-30	changement parametres inductifs dans les theories	mohring
2005-08-26	* empty log message *	letouzey
2005-07-15	Fix sumbool_not hint (on behalf of cpaulin).	coq
2005-07-15	add a left and right tactic for classical logic	narboux
2005-07-13	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-05-19	Documentation	herbelin
2005-05-17	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin
2005-05-02	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-04-26	Fixed hypotheses of Z_lt_induction (see #957)	herbelin
2005-03-31	Added option_map	herbelin
2005-03-29	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-24	Missing translating a 'O' into a '0'	herbelin
2005-03-16	MAJ PolyList -> List	herbelin
2005-02-23	quelques tactics ltac	letouzey
2005-02-07	Re-unboxing de BinPos (sauf Pplus): sinon, fait partir Coqbook pour des jours...	coq
2005-02-04	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-03	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
2004-12-19	In_dec transparent (wish #902)	herbelin
2004-12-06	Inutile de réserver les notations à base de '{ }'	herbelin
2004-12-05	MAJ changements ChoiceFacts	herbelin
2004-12-05	Paramétrisation du domaine des axiomes de choix + ajout description = choice...	herbelin
2004-11-22	compatibility with POWERPC	gregoire
2004-11-19	Généralisation à Type de certaines propriétés des relations	herbelin
2004-11-16	Copy of the definition of prodT (already in the standard library) removed.	sacerdot
2004-11-12	Changement dans les boxed values .	gregoire
2004-11-07	MAJ commentaire sur incohérence EM dans Set	herbelin
2004-11-02	Réponse à la conjecture que PI est indépendant de EM dans CC	herbelin
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-10-19	Proof term size reduction (again).	sacerdot
2004-10-18	* Code simplification and clean-up. In particular there is no more code	sacerdot
2004-10-11	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin
2004-10-07	iff and impl are now declared as transitive relations.	sacerdot
2004-10-06	* New syntactic sugar: Add Relation ... transitivity proved by ...	sacerdot
2004-10-06	added transitivity	barras
2004-09-29	impl is a reflexive relation (it used to be areflexive).	sacerdot