coq - The formal proof system

Age	Commit message (Expand)	Author
2006-03-05	Ajout test relatif au bug #984	herbelin
2006-03-02	Ajout test bug 1089	herbelin
2006-03-02	Correction du bug 808: il est maintenant interdit de déclarer une assomption...	coq
2006-03-01	Correction bug #842 (rename d'une hyp du contexte)	herbelin
2006-01-30	Prise en compte coercions autour des sous-termes filtrés (si non dépendants)	herbelin
2006-01-23	Répercussion mise à jour de Pierre Casteran vis à vis du changement de sta...	herbelin
2006-01-20	Test bug 983	herbelin
2006-01-15	Test utf-8	herbelin
2006-01-11	Test conflictuel - ajouté pour mémoire	herbelin
2006-01-11	Test or-patterns	herbelin
2005-12-30	Test bug #1025	herbelin
2005-12-27	Mini-test d'extraction	herbelin
2005-12-21	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin
2005-12-21	Activation du test de Refine en v7 pour mémoire avant passage à la v8	herbelin
2005-11-03	* empty log message *	mohring
2005-11-02	Test reproductibilité du bug #1031	herbelin
2005-09-09	Declare Implicit Tactic	herbelin
2005-09-09	Suppression test CCSolve car remplaçé par Congruence mais qui ne traite pas...	herbelin
2005-09-08	Test clear final dans intros pattern	herbelin
2005-05-19	A wish by Bas Spitters granted: a little more of unification up to	sacerdot
2005-05-18	Implemented autorewrite with ... in hyp [using ...].	sacerdot
2005-03-21	Ajout Unset Implicit Arguments manquant	herbelin
2005-03-20	Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des hyps...	herbelin
2005-03-19	Ajout test bug #935	herbelin
2005-03-17	Nouvelle syntaxe 'with' des modules non gérée en v7	herbelin
2005-03-16	Nouvelle syntaxe 'with' des modules non gérée en v7	herbelin
2005-03-08	Fix bug #931: leave dependent evars as such for refine	herbelin
2005-02-21	* empty log message *	herbelin
2005-02-17	Test bug #922	herbelin
2005-02-02	test de la bonne position des vars de ltac entre les vars et les rels	herbelin
2005-01-12	The new tutorial on (co)inductive types by Pierre Casteran.	sacerdot
2004-12-08	Ajout bug do_restrict_hyp	herbelin
2004-12-06	Erreur commit précédent	herbelin
2004-12-06	Ajout bug #888	herbelin
2004-12-06	Ajout bug #889	herbelin
2004-12-04	Failed in 8.0pl1	herbelin
2004-12-03	Was failing in 8.0pl1	herbelin
2004-10-27	Ajout test dependent rewrite	herbelin
2004-10-14	reflexivity, symmetry, symmetry ... in e transitivity now fall-back	sacerdot
2004-10-07	New commands	sacerdot
2004-10-04	Added "as ..." parameter to Add Morphism.	sacerdot
2004-10-01	Added "as ..." parameters to "Add Setoid"	sacerdot
2004-09-30	New tactic	sacerdot
2004-09-30	New tactic [setoid_]rewrite ... in ... [generate side conditions ...].	sacerdot
2004-09-29	Test updated.	sacerdot
2004-09-25	Ajouts	herbelin
2004-09-24	Ajout bug #255	herbelin
2004-09-03	* 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-08-23	The previous test file was truncated. New commit to fix the previous	sacerdot