coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Cleaning code and comment.	courtieu	2007-10-30
*	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-25
*	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-24
*	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-21
*	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-18
*	Repair Haskell/Scheme extraction in the new extraction backend design:	letouzey	2007-10-17
*	Major reorganisation of the extraction "backend".	letouzey	2007-10-17
*	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-16
*	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-09
*	Better use of tables for storing results of extract_ind (bug #1709)	letouzey	2007-10-08
*	Allowing infix constructors/types in a Extract Inductive	letouzey	2007-10-06
*	Extraction: factorisation of identical branches in a match	letouzey	2007-10-06
*	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin	2007-10-03
*	Complément nécessaire aux révisions 10156 et 10157	herbelin	2007-10-01
*	Modification of the Scheme command.	vsiles	2007-09-28
*	curpat_ty was in a smaller context	msozeau	2007-09-21
*	Changed the definition of Nminus in BinNat.v by removing comparison.	emakarov	2007-09-20
*	Raffinement de l'algorithme d'inférence de type	herbelin	2007-09-17
*	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey	2007-09-15
*	Correction du bug #1679 (congruence) et ajout test-suite	corbinea	2007-09-14
*	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-09-06
*	fin de la correction de Function	jforest	2007-08-31
*	correction bug d'efficacite dans Function	jforest	2007-08-31
*	Oubli dans commit 10102...	herbelin	2007-08-30
*	- Débogueur: positionnement de set_detype_anonymous pour ne pas	herbelin	2007-08-29
*	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-27
*	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-26
*	Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;	notin	2007-08-16
*	Fix dependency bugs due to Program modules renamings.	msozeau	2007-08-08
*	Move Program tactics into a proper theories/ directory as they are general pu...	msozeau	2007-08-07
*	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-24
*	Documentation of Program and its tactics, fix enormous interaction bug due to...	msozeau	2007-07-19
*	A generic preprocessing tactic zify for (r)omega	letouzey	2007-07-18
*	Generalized CAMLP4USE for pp dependencies	corbinea	2007-07-16
*	some more useless constant in const_omega	letouzey	2007-07-13
*	Beginning of a reorganisation of the ml part for romega:	letouzey	2007-07-13