coq - The formal proof system

Age	Commit message (Expand)	Author
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
2007-11-07	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10300 85f007b7-540e-0...	emakarov
2007-11-07	Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v.	emakarov
2007-11-07	Replaced BinNat with a new version that is based on theories/Numbers/Natural/...	emakarov
2007-11-07	bug in infos_and_sort: type of constructor was not reduced enough	barras
2007-11-06	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey
2007-11-06	bugs dp	filliatr
2007-11-06	Oups. Clflags.recursive_types isnt normally accessible on a standard ocaml in...	letouzey
2007-11-06	Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...	letouzey
2007-11-06	useless Require Export Extraction	letouzey