coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	New commands	sacerdot	2004-10-07
*	Added "as ..." parameter to Add Morphism.	sacerdot	2004-10-04
*	Added "as ..." parameters to "Add Setoid"	sacerdot	2004-10-01
*	New tactic	sacerdot	2004-09-30
*	New tactic [setoid_]rewrite ... in ... [generate side conditions ...].	sacerdot	2004-09-30
*	Test updated.	sacerdot	2004-09-29
*	Ajouts	herbelin	2004-09-25
*	Ajout bug #255	herbelin	2004-09-24
*	* New test (for setoid_replace in the general case)	sacerdot	2004-09-03
*	* setoid_test.v removed and added again in new syntax	sacerdot	2004-09-03
*	The previous test file was truncated. New commit to fix the previous	sacerdot	2004-08-23
*	Several tests for the bug-fixed and improved new version of	sacerdot	2004-07-23
*	Nouvelle en-tête	herbelin	2004-07-16
*	commentaire	herbelin	2004-06-02
*	Ajout tests affichage coercions vers Funclass	herbelin	2004-06-02
*	Ajout tests	herbelin	2004-06-02
*	Protection du destruct pour vérifier que ce n'est pas une anomalie, à défa...	herbelin	2004-05-20
*	Points-fixes avec let-in	herbelin	2004-05-03
*	Ajout test bug 711	herbelin	2004-05-02
*	Test bug 705	herbelin	2004-04-29
*	Ajout test If nouvelle syntaxe	herbelin	2004-04-28
*	Ajout exemple Bruno	herbelin	2004-04-14
*	* empty log message *	barras	2004-03-26
*	* empty log message *	barras	2004-03-24
*	bug de PP des fix (coqbugs #574)	barras	2004-03-24
*	Nouvel exemple; correction du contexte du précédent	herbelin	2004-03-13
*	Corrections	herbelin	2004-03-12
*	Test l'interprétation des scopes	herbelin	2004-03-11
*	Ajout exemple Inst	herbelin	2004-03-11
*	Ajout vieil exemple de coq-club	herbelin	2004-03-11
*	Ajout d'un vieil exemple de N. Magaud	herbelin	2004-03-11
*	Ajout bug #540	herbelin	2004-03-11
*	the output the parser should produce now	bertot	2004-03-06
*	changed the test for obj_magic.v to be less sensitive to changes	bertot	2004-03-06
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Exemple de Frederic	herbelin	2004-02-28
*	Ajout test synthese du predicat a partir du cast d'un filtrage avec dependances	herbelin	2004-02-27
*	New version of Functional Scheme and functional induction. Deals with	coq	2004-02-09
*	Test dependencies in constructors	herbelin	2004-02-06
*	Ajout filtrage sur motifs dépendants dans des inductifs différents	herbelin	2004-02-06
*	Vérification de la prise en compte des termes de type non inductif	herbelin	2004-02-04
*	[ -d ... ] au lieu de [ -f ... ] sur commit précédént	herbelin	2004-01-01
*	Protection contre l'echec des tests parser pour la distrib	herbelin	2003-12-27
*	Suppression en v8	herbelin	2003-12-27
*	BUG	herbelin	2003-12-24
*	Bug commit precedent	herbelin	2003-12-23
*	Renommages des hypotheses transformees car en raison des possibles dependance...	herbelin	2003-12-23
*	ajout test de non-regression Clear d'une def locale	barras	2003-12-17
*	Ajout exemple Yves	herbelin	2003-12-12
*	Pour eviter d'avoir un gros type dans Set	herbelin	2003-12-05