coq - The formal proof system

Age	Commit message (Expand)	Author
2009-11-02	Remove various useless {struct} annotations	letouzey
2009-10-08	Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-09	Znumtheory + Zdiv enriched with stuff from ZMicromega, misc improvements	letouzey
2008-07-24	Tauto breaking not only binary "conjunctions" seems like a bad idea	msozeau
2008-07-23	Oops... forgot some debug code.	msozeau
2008-07-22	A try at allowing matching on applications as a binary syntax node by default.	msozeau
2007-11-06	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey
2007-11-06	Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...	letouzey
2007-11-01	In agreement with Laurent Thery, start migration of auxiliary results	letouzey
2006-10-17	Mise en forme des theories	notin
2006-09-26	commit de field + renommages	barras
2006-09-26	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras
2006-06-26	Ajout de Zgcd_spec (compat.)	notin
2006-06-25	nouvel algorithme pour Zgcd (plus rapide) + un Qcompare	letouzey
2006-05-23	Changement de prÃ©cÃ©dence de l'argument du by de assert; consÃ©quences...	herbelin
2006-05-14	On remet plutot l'ancien nom Zgcd_is_pos au lieu de Zgcd_pos	letouzey
2006-05-13	typo	letouzey
2006-05-13	un Zgcd calculant dans coq	letouzey
2006-05-11	une fonction pouvant calculer le gcd en coq	letouzey
2006-05-05	un Zgcd general gardant trace des coefs	letouzey
2005-05-02	Finalement, préservation de la compatibilité pour Z_lt_induction et ajout p...	herbelin
2005-04-26	Fixed hypotheses of Z_lt_induction (see #957)	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2003-12-16	Duplication temporaire des règles de syntaxe des paires	herbelin
2003-12-04	Suppression du niveau 250 vide car pose des problemes avec camlp4; remplace p...	herbelin
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2003-11-29	Report de lemmes de Znumtheory dans Zabs ou BinInt	herbelin
2003-11-19	ajout de Znumtheory.v dans ZArith	letouzey