coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	removing a warning at compilation time	jforest	2007-07-13
*	Deletion of contrib/extraction/test	letouzey	2007-07-12
*	normalisation (by closure) was not performed under fixpoints	barras	2007-07-12
*	port de r9968: bug avec les ring calculatoires	barras	2007-07-12
*	An optimization to simplify generated obligations removing unnecessary let-in's.	msozeau	2007-07-12
*	Fix bug when adding progs with no obligations	msozeau	2007-07-12
*	Remove dead modules in Subtac.	msozeau	2007-07-12
*	Cleanup, use Util list functions when possible	msozeau	2007-07-12
*	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey	2007-07-11
*	Big reorganization of romega/ReflOmegaCore.v: towards a modular	letouzey	2007-07-10
*	Improvements / Bug fixes for ROmega	letouzey	2007-07-09
*	minor bug correction (continuing r 9943)	jforest	2007-07-06
*	Adding a syntax for "n-ary" rewrite:	letouzey	2007-07-06
*	sequel to commit 9952: forgot to adapt xlate to the new n-ary rename	letouzey	2007-07-06