coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	* 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
*	Proof term size reduction (again).	sacerdot	2004-10-19
*	* Code simplification and clean-up. In particular there is no more code	sacerdot	2004-10-18
*	'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...	herbelin	2004-10-11
*	iff and impl are now declared as transitive relations.	sacerdot	2004-10-07
*	* New syntactic sugar: Add Relation ... transitivity proved by ...	sacerdot	2004-10-06
*	added transitivity	barras	2004-10-06
*	impl is a reflexive relation (it used to be areflexive).	sacerdot	2004-09-29
*	impl relation and impl/and/or/not morphisms over impl declared.	sacerdot	2004-09-29
*	* cleaning/renaming	sacerdot	2004-09-08
*	The Coq part of the reflexive tactic is now able to handle also	sacerdot	2004-09-08
*	* The Coq part of the reflexive tactic setoid_rewrite is generalized to	sacerdot	2004-09-07
*	New reflexive implementation of setoid_rewrite. The new implementation	sacerdot	2004-09-03
*	Zbool déjà dans ZArith_base	herbelin	2004-08-03
*	Minimisation utilisation NNPP	herbelin	2004-08-03
*	Déclaration d'obsolescence	herbelin	2004-08-03
*	Typo	herbelin	2004-08-03
*	Ref	herbelin	2004-08-03