coq - The formal proof system

Age	Commit message (Expand)	Author
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-11-27	bug correction in functional inversion principle generation	jforest
2007-11-26	minor bug correction in Function	jforest
2007-11-21	Extraction inlines Wf.Fix by default (wish of Y.Bertot)	letouzey
2007-11-19	Bug in functionnal induction principle generation	jforest
2007-11-13	Correcting a segfault on amd64 arch with native compiler of ocaml 3.10	jforest
2007-11-09	Nettoyage de Print Assumptions :	aspiwack
2007-11-08	Prise en compte des notations "alias" dans la globalisation des coercions.	herbelin
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	Replaced BinNat with a new version that is based on theories/Numbers/Natural/...	emakarov
2007-11-06	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey
2007-11-06	bugs dp	filliatr
2007-11-06	useless Require Export Extraction	letouzey
2007-11-04	Fix bug#1739	msozeau
2007-10-30	Cleaning code and comment.	courtieu
2007-10-25	small fix of commit 10188: a string given via Extract Inductive can be empty	letouzey
2007-10-25	Added NIso.v to Makefile.common. Changed Examples.v in contrib/micromega to u...	emakarov
2007-10-24	Fix define body bug fix	msozeau
2007-10-24	Fix define body bug	msozeau
2007-10-24	Fix some bugs, add possibility of automatically solving a proof statement's o...	msozeau
2007-10-21	An error message instead of an empty extraction when the monolithic	letouzey
2007-10-21	Avoid the auto-inlining of small fixpoints like List.map.	letouzey
2007-10-18	Changed RingMicromega to use NRing instead of Ring_polynom. NRing is a versio...	emakarov
2007-10-18	added generation from trivial patterns for congruence	corbinea
2007-10-17	Repair Haskell/Scheme extraction in the new extraction backend design:	letouzey
2007-10-17	Major reorganisation of the extraction "backend".	letouzey
2007-10-16	Fixed congruence instance generator + changed default depth to 1000	corbinea
2007-10-16	Added transitivity and irreflexivity of <, as well as < -elimination for bina...	emakarov
2007-10-09	Extraction now checks that the required libraries are indeed loaded (bug #1144)	letouzey
2007-10-09	forbid extraction under a module type	letouzey
2007-10-09	Extract Inline/Inductive/Constant can now be used from inside a module	letouzey
2007-10-08	Better use of tables for storing results of extract_ind (bug #1709)	letouzey
2007-10-06	Allowing infix constructors/types in a Extract Inductive	letouzey
2007-10-06	Extraction: factorisation of identical branches in a match	letouzey
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-10-01	Complément nécessaire aux révisions 10156 et 10157	herbelin
2007-09-28	Modification of the Scheme command.	vsiles
2007-09-21	curpat_ty was in a smaller context	msozeau
2007-09-20	Changed the definition of Nminus in BinNat.v by removing comparison.	emakarov
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-09-15	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey
2007-09-14	Correction du bug #1679 (congruence) et ajout test-suite	corbinea
2007-09-06	errors in recdef.ml4:	bertot
2007-09-06	this should fix a problem described in a message by Dufourd on July 30th, 2007	bertot
2007-08-31	fin de la correction de Function	jforest
2007-08-31	correction bug d'efficacite dans Function	jforest
2007-08-30	Oubli dans commit 10102...	herbelin
2007-08-29	- Débogueur: positionnement de set_detype_anonymous pour ne pas	herbelin