coq - The formal proof system

Age	Commit message (Expand)	Author
2003-03-29	indentation	herbelin
2003-03-14	* empty log message *	barras
2003-03-04	MAJ	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-02-06	commentaire	coq
2003-01-31	MAJ syntaxe modules + nouveau fichier mod_decl qui explique tout	coq
2003-01-30	Pb de parenthèse dans "Check (S (plus O O))"	herbelin
2003-01-28	MAJ pour Reg	desmettr
2003-01-22	* empty log message *	barras
2003-01-20	* empty log message *	herbelin
2003-01-19	Tests ltac	herbelin
2003-01-19	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin
2003-01-16	* empty log message *	herbelin
2003-01-15	Problème de désynchronisation des variables du type et du corps d'un point-...	herbelin
2003-01-15	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin
2003-01-09	Export M + Module M <: SIG	coq
2002-12-12	Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la nouvelle...	desmettr
2002-12-09	Add an example with Ring.	bertot
2002-12-02	MAJ sur MAJ	herbelin
2002-12-02	Remplacement de Syntactic Definition par Notation	herbelin
2002-11-25	MAJ	herbelin
2002-11-24	MAJ	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-29	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	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-16	Parseur pour n>20 dans nat plus disponible	herbelin
2002-10-06	correcting the treatment of many tactics that use quant_hyp in file xlate.ml	bertot
2002-10-01	Adding the congruence closure tactics (CC and CCsolve).	corbinea
2002-09-27	Encore quelques rangements dans Nametab + petits trucs	coq
2002-09-21	Changement de sémantique de Remark : maintenant un global comme les autres	herbelin
2002-08-21	Correction	coq
2002-08-16	Encore quelques tests sur modules...	coq
2002-08-15	Test for redundant clauses	herbelin
2002-08-14	Test affichage optimal des coercions	herbelin
2002-08-13	Petites corrections ici et la	coq
2002-08-02	Modules dans COQ\!\!\!\!	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-21	Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement	filliatr
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	Locate n'échoue plus: déplacement de Remark1 et Remark2 dans output	herbelin