coq - The formal proof system

Age	Commit message (Expand)	Author
2005-11-03	* empty log message *	mohring
2005-11-03	deplacement params_ind	mohring
2005-11-02	Test reproductibilité du bug #1031	herbelin
2005-11-02	Ajout tests interactifs	herbelin
2005-11-01	Interactive test of Back	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-23	Consequence of allowing the numerical argument of auto to be an ident for ltac	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-22	Suppression des fichiers temporaires	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-27	Ajout test bug 860	herbelin
2004-12-09	Réactivation des tests output avec test aussi de la nouvelle syntaxe	herbelin
2004-12-09	Ajout d'une version nouvelle syntaxe	herbelin
2004-12-09	MAJ avec les particularités de l'afficheur v7 de la V8	herbelin
2004-12-09	Test d'affichage d'un Fix donné avec /n	herbelin
2004-12-09	Fichier non traductible (référence à des objets invisibles ce qui empêche...	herbelin
2004-12-09	Intégré à Implicit.v	herbelin
2004-12-09	Ajout suffixe 8 pour test en nouvelle syntaxe	herbelin
2004-12-09	Plus de statut spécial pour Remark	herbelin
2004-12-09	Désactivation du test du printer arithmétique v7	herbelin
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-11-28	Suppression bruit perl	herbelin
2004-11-28	Re-commit version nouvelle syntaxe	herbelin
2004-11-28	Passage à la v8 pour test parser	herbelin
2004-11-17	Test lieurs dans Notation	herbelin
2004-11-17	test-suite/output/Notations.out	herbelin
2004-10-27	Ajout test dependent rewrite	herbelin
2004-10-17	* empty log message *	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