coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Commentaires coqdoc	herbelin	2004-08-01
*	Commentaires coqdoc	herbelin	2004-08-01
*	Nouvelle en-tête	herbelin	2004-07-16
*	simplified proof (eq and eqT are now the same)	barras	2004-06-25
*	Nouveaux thms de non circularité de nat	herbelin	2004-06-02
*	eq2eqT et eqT2eq devenus obsolètes	herbelin	2004-06-02
*	sumbool et sumor affich avec 'if' si possible	herbelin	2004-04-06
*	Commentaires	herbelin	2004-03-29
*	Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...	herbelin	2004-03-28
*	MAJ commentaires	herbelin	2004-03-24
*	Definition de la notation de la paire par un motif recursif	herbelin	2004-03-17
*	Commentaires	herbelin	2004-03-17
*	ajout decimal_exp pour interpreter les notations decimales	mohring	2004-03-12
*	ide: silent behavior better, save icon, -byte works	marche	2004-03-03
*	MAJ Commentaires	herbelin	2004-02-28
*	Ajout delimiteur pour bool_scope	herbelin	2004-02-12
*	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin	2004-02-12