coq - The formal proof system

Age	Commit message (Expand)	Author
2007-12-21	Deux petits théorèmes utiles dans Minus.v	notin
2007-12-21	Ajouts de quelques tests sur les bugs	notin
2007-12-19	Suppression de commentaires inutiles	notin
2007-12-18	Correction du bug #1745 (installation des fichiers .vo de Numbers)	notin
2007-12-18	Petite correction sur coq_makefile	notin
2007-12-18	Maj du lien vers coq-bugs dans Coqide.	glondu
2007-12-18	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack
2007-12-17	Print Assumptions est pret pour la release.	aspiwack
2007-12-17	Correction d'un bug dans Coqdoc: les mots clés liés aux sections étaient s...	notin
2007-12-17	Quelques arguments en plus...	glondu
2007-12-14	Correction ordre d'affichage des champs des Record	herbelin
2007-12-14	Petite correction de Option.default (default faisait un Option.map	aspiwack
2007-12-13	migration of ide/utf8.v to theories/Unicode/Utf8.v	letouzey
2007-12-12	Ajout d'un test pour le bug #1100	notin
2007-12-11	Test pour le bug #1754	notin
2007-12-11	Modification de la question no 172 de la FAQ (cf bug #1755)	notin
2007-12-07	Adding the tactic "instantiate" (without argument), to force the	glondu
2007-12-07	Ocaml toplevel convenience.	glondu
2007-12-07	Util.option_compare devient Option.Misc.Compare et change un peu de type	aspiwack
2007-12-07	Petit oubli de thery.	glondu
2007-12-06	Adding MemoFunction + Lowering Height	thery
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2007-12-06	Commit intermédiaire express de réparation de coqide.ml, que j'avais	aspiwack
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-11-28	Ajout de l'axiomatisation des entiers à la documentation de la librairie sta...	notin
2007-11-27	bug correction in functional inversion principle generation	jforest
2007-11-26	minor bug correction in Function	jforest
2007-11-24	* A few Parameter Inline, but they dont seem to help much concerning	letouzey
2007-11-24	small improvements about Qc. Beware: Qlt_trans becomes Qclt_trans (as it ough...	letouzey
2007-11-22	An update on Numbers. Added two files dealing with recursion, for information...	emakarov
2007-11-21	Extraction inlines Wf.Fix by default (wish of Y.Bertot)	letouzey
2007-11-21	extensible version	thery
2007-11-19	Bug in functionnal induction principle generation	jforest
2007-11-16	Added theorems; created NZPlusOrder from NTimesOrder.	emakarov
2007-11-15	Split NTimesOrder into properly NTimesOrder and NPlusOrder.	emakarov
2007-11-14	Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ZArith/Zorder...	emakarov
2007-11-13	Correcting a segfault on amd64 arch with native compiler of ocaml 3.10	jforest
2007-11-12	Correction du bug #1741	notin
2007-11-10	A result about Zsgn(a/b), both for Zdiv and ZOdiv	letouzey
2007-11-10	First reasonably complete version of ZOdiv, including some properties	letouzey
2007-11-09	Nettoyage de Print Assumptions :	aspiwack
2007-11-09	Suite ajout raccourcis à compute et lazy pour réduire tout sauf	herbelin
2007-11-09	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10309 85f007b7-540e-0...	jforest
2007-11-09	Rétablissement compatibilité constr_of_reference	herbelin
2007-11-09	more about ZOdiv and ZOmod (still not finished)	letouzey
2007-11-08	Corrected the ML code for well-founded recursion in the comment.	emakarov
2007-11-08	Prise en compte des notations "alias" dans la globalisation des coercions.	herbelin
2007-11-08	Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.	emakarov
2007-11-08	setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def.	letouzey
2007-11-08	small copy&paste bug in zify: some Pmult should be Nmult	letouzey