coq - The formal proof system

Age	Commit message (Expand)	Author
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
2007-08-27	Oubli dans la révision 10098 (nettoyage body_of_type)	herbelin
2007-08-27	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin
2007-08-26	Fix bug on wellfounded defs with constant parameters and dependencies on the ...	msozeau
2007-08-26	Fix de Bruijn bug in wf definitions.	msozeau
2007-08-26	Fix evars bug in mutual fixpoints with implicit types and bug in inequalities...	msozeau
2007-08-16	Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;	notin
2007-08-08	Fix dependency bugs due to Program modules renamings.	msozeau
2007-08-07	Move Program tactics into a proper theories/ directory as they are general pu...	msozeau
2007-07-24	fixed bug 1448 and 1674	barras
2007-07-24	fixed bug 1675: computing carrier from the relation type was not right	barras
2007-07-24	Declarative language: fixed the generation of fixpoints for induction proofs.	corbinea
2007-07-19	Documentation of Program and its tactics, fix enormous interaction bug due to...	msozeau
2007-07-18	A generic preprocessing tactic zify for (r)omega	letouzey
2007-07-16	Generalized CAMLP4USE for pp dependencies	corbinea
2007-07-13	some more useless constant in const_omega	letouzey
2007-07-13	Beginning of a reorganisation of the ml part for romega:	letouzey