coq - The formal proof system

Age	Commit message (Expand)	Author
2003-03-29	indentation	herbelin
2003-02-28	fixing a typo in the new Funinv.v test in test-suite/success	courtieu
2003-02-27	Adding tests for the "functional induction" facility.	bertot
2003-01-28	MAJ pour Reg	desmettr
2003-01-22	* empty log message *	barras
2003-01-19	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin
2003-01-15	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin
2002-12-12	Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la nouvelle...	desmettr
2002-12-02	MAJ sur MAJ	herbelin
2002-12-02	Remplacement de Syntactic Definition par Notation	herbelin
2002-11-24	Remplacement de Syntactic Definition par Notation	herbelin
2002-11-06	Test de la correction d'un bug soumis par Dachuan Yu	herbelin
2002-10-23	Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...	herbelin
2002-10-21	Parenthèses manquantes pour se conformer à la doc (et au nouveau PeanoSynta...	herbelin
2002-10-01	Adding the congruence closure tactics (CC and CCsolve).	corbinea
2002-09-27	Encore quelques rangements dans Nametab + petits trucs	coq
2002-07-22	* empty log message *	desmettr
2002-07-19	correction bugs Tauto	courant
2002-07-18	* empty log message *	desmettr
2002-07-05	* empty log message *	corbinea
2002-07-05	Added a new uncompleteness bug found in Tauto.	corbinea
2002-06-14	* empty log message *	herbelin
2002-06-13	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-11	Tests pour la tactique Reg	desmettr
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-06	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-05	Fusion entre la nouvelle et l'ancienne syntaxe de HintDestruct	herbelin
2002-05-29	* empty log message *	herbelin
2002-02-28	* empty log message *	herbelin
2002-01-25	* empty log message *	herbelin
2002-01-21	Ajout test de Pierre Crégut	herbelin
2002-01-18	* empty log message *	herbelin
2002-01-18	* empty log message *	herbelin
2002-01-16	Ajout d'un test sur les anonymes dépendant dans des arguments implicites	herbelin
2002-01-15	Test le filtrage dépendant vers l'avant	herbelin
2001-12-21	* empty log message *	herbelin
2001-12-21	Ajout d'un exemple de Christine	herbelin
2001-12-19	MAJ Grammar	herbelin
2001-12-19	NatRing (2ème)	herbelin
2001-12-19	NatRing	herbelin
2001-12-19	Un peu plus d'inférence des ? traitée par le Cases	herbelin
2001-12-13	* empty log message *	herbelin
2001-12-11	Test des coercions dans les motifs	herbelin
2001-11-21	* empty log message *	herbelin
2001-11-21	La synthèse des '?' dans l'exemple avec un let était un peu trop ambitieuse...	herbelin
2001-11-21	Un bug dans le script	herbelin