coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	* empty log message *	mohring	2005-11-03
*	deplacement params_ind	mohring	2005-11-03
*	Test reproductibilité du bug #1031	herbelin	2005-11-02
*	Ajout tests interactifs	herbelin	2005-11-02
*	Interactive test of Back	herbelin	2005-11-01
*	Declare Implicit Tactic	herbelin	2005-09-09
*	Suppression test CCSolve car remplaçé par Congruence mais qui ne traite pas...	herbelin	2005-09-09
*	Test clear final dans intros pattern	herbelin	2005-09-08
*	Consequence of allowing the numerical argument of auto to be an ident for ltac	herbelin	2005-05-23
*	A wish by Bas Spitters granted: a little more of unification up to	sacerdot	2005-05-19
*	Implemented autorewrite with ... in hyp [using ...].	sacerdot	2005-05-18
*	Ajout Unset Implicit Arguments manquant	herbelin	2005-03-21
*	Test d'un bug de 'Inv.dependent_hyps' qui ne met pas à jour le type des hyps...	herbelin	2005-03-20
*	Ajout test bug #935	herbelin	2005-03-19
*	Nouvelle syntaxe 'with' des modules non gérée en v7	herbelin	2005-03-17
*	Nouvelle syntaxe 'with' des modules non gérée en v7	herbelin	2005-03-16
*	Fix bug #931: leave dependent evars as such for refine	herbelin	2005-03-08
*	Suppression des fichiers temporaires	herbelin	2005-02-22
*	* empty log message *	herbelin	2005-02-21
*	Test bug #922	herbelin	2005-02-17
*	test de la bonne position des vars de ltac entre les vars et les rels	herbelin	2005-02-02
*	The new tutorial on (co)inductive types by Pierre Casteran.	sacerdot	2005-01-12
*	Ajout test bug 860	herbelin	2004-12-27
*	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-09
*	Ajout bug do_restrict_hyp	herbelin	2004-12-08
*	Erreur commit précédent	herbelin	2004-12-06
*	Ajout bug #888	herbelin	2004-12-06
*	Ajout bug #889	herbelin	2004-12-06
*	Failed in 8.0pl1	herbelin	2004-12-04
*	Was failing in 8.0pl1	herbelin	2004-12-03
*	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-28
*	Test lieurs dans Notation	herbelin	2004-11-17
*	test-suite/output/Notations.out	herbelin	2004-11-17
*	Ajout test dependent rewrite	herbelin	2004-10-27
*	* empty log message *	herbelin	2004-10-17
*	reflexivity, symmetry, symmetry ... in e transitivity now fall-back	sacerdot	2004-10-14
*	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