coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Test de la correction d'un bug soumis par Dachuan Yu	herbelin	2002-11-06
*	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin	2002-10-29
*	Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...	herbelin	2002-10-23
*	Parenthèses manquantes pour se conformer à la doc (et au nouveau PeanoSynta...	herbelin	2002-10-21
*	Parseur pour n>20 dans nat plus disponible	herbelin	2002-10-16
*	correcting the treatment of many tactics that use quant_hyp in file xlate.ml	bertot	2002-10-06
*	Adding the congruence closure tactics (CC and CCsolve).	corbinea	2002-10-01
*	Encore quelques rangements dans Nametab + petits trucs	coq	2002-09-27
*	Changement de sémantique de Remark : maintenant un global comme les autres	herbelin	2002-09-21
*	Correction	coq	2002-08-21
*	Encore quelques tests sur modules...	coq	2002-08-16
*	Test for redundant clauses	herbelin	2002-08-15
*	Test affichage optimal des coercions	herbelin	2002-08-14
*	Petites corrections ici et la	coq	2002-08-13
*	Modules dans COQ\!\!\!\!	coq	2002-08-02
*	* empty log message *	desmettr	2002-07-22
*	correction bugs Tauto	courant	2002-07-19
*	* empty log message *	desmettr	2002-07-18
*	* empty log message *	corbinea	2002-07-05
*	Added a new uncompleteness bug found in Tauto.	corbinea	2002-07-05
*	Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement	filliatr	2002-06-21
*	* empty log message *	herbelin	2002-06-14
*	Test de l'interprétation des fermetures de Match Context (2ème)	herbelin	2002-06-13
*	Test de l'interprétation des fermetures de Match Context	herbelin	2002-06-13
*	Tests pour la tactique Reg	desmettr	2002-06-11
*	Locate n'échoue plus: déplacement de Remark1 et Remark2 dans output	herbelin	2002-06-07
*	I added a comment on the tactic compute_POS.	bertot	2002-06-07
*	This example does not work in coq-7.3, but does in coq-7.2.	bertot	2002-06-07
*	Ajout exemple JCF conflit variable interne, variable de section	herbelin	2002-06-06
*	Des exemples sérieux	herbelin	2002-06-06
*	Ajout exemple Yves renommage différent d'une var de section	herbelin	2002-06-06
*	Fusion entre la nouvelle et l'ancienne syntaxe de HintDestruct	herbelin	2002-06-05
*	* empty log message *	herbelin	2002-06-03
*	* empty log message *	herbelin	2002-05-29
*	Quelques bugs avec inject_nat	herbelin	2002-04-17
*	* empty log message *	herbelin	2002-04-12
*	* empty log message *	herbelin	2002-02-28
*	Test affichage O de nat dans une expression sur Z	herbelin	2002-01-25
*	* empty log message *	herbelin	2002-01-25
*	Ajout test de Pierre Crégut	herbelin	2002-01-21
*	* empty log message *	herbelin	2002-01-18
*	* empty log message *	herbelin	2002-01-18
*	Ajout d'un test sur les anonymes dépendant dans des arguments implicites	herbelin	2002-01-16
*	Test le filtrage dépendant vers l'avant	herbelin	2002-01-15
*	* empty log message *	herbelin	2001-12-21
*	Ajout d'un exemple de Christine	herbelin	2001-12-21
*	Test sobriété de la réduction de Intuition	herbelin	2001-12-19
*	Test sobriété de la réduction de Intuition	herbelin	2001-12-19
*	MAJ Grammar	herbelin	2001-12-19
*	NatRing (2ème)	herbelin	2001-12-19