coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Delayed the computation of parameters in sort polymorphism of	herbelin	2013-05-14
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Minor code cleaning in CArray / CList.	ppedrot	2013-03-23
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Array.create is deprecated	pboutill	2012-12-19
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (kernel)	ppedrot	2012-11-22
*	More monomorphizations	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Noise for nothing	pboutill	2012-03-02
*	It happens that the type inference algorithm (pretyping) did not check	herbelin	2011-10-05
*	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey	2011-07-04
*	Univ.constraints made fully abstract instead of being a Set of abstract stuff	letouzey	2010-12-18
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	"Improved" the form of the inferred type of "match" by	herbelin	2010-06-03
*	fixed guard check with commutative cuts	barras	2010-05-20
*	Applicative commutative cuts in Fixpoint guard condition	pboutill	2010-05-18
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	fixed confusion between number of cstr arguments and number of pattern variab...	barras	2010-03-12
*	introduced lazy computation of size info in the guard condition	barras	2010-03-11
*	revert on commit r12553	barras	2009-12-07
*	two improvements of the guard condition:	barras	2009-12-01
*	This big commit addresses two problems:	soubiran	2009-10-21
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Ensures that let-in's in arities of inductive types work well. Maybe not	herbelin	2009-08-11
*	- Fixing bug #2139 (kernel-based test of well-formation of elimination	herbelin	2009-07-15
*	fixed kernel bug (de Bruijn) + test-suite	barras	2008-12-02
*	fixing r11433 again:	barras	2008-10-07
*	fixed pb with r11433	barras	2008-10-07
*	bug #1951: polymorphic indtypes: universe subst was not performed in the type...	barras	2008-10-06
*	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin	2008-07-25
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	Changement de stratégie vis à vis du commit 10859 sur la gestion des	herbelin	2008-05-12
*	Correction du bug des types singletons pas sous-type de Set	herbelin	2008-04-27
*	Prise en compte des coercions dans les clauses "with" même si le type	herbelin	2008-04-23
*	improved the implementation of rtree	barras	2008-03-18
*	Add more information to IllFormedRecBody exceptions, to show the exact	msozeau	2008-02-08
*	Correction bug 1718 (lazy delta unfolding used to miss delta on rels and vars)	herbelin	2007-10-04
*	cosmetique	barras	2006-12-12
*	bug condition de garde	barras	2006-12-08
*	Débranchement du polymorphisme de sorte sur les définitions dans Type	herbelin	2006-10-30
*	Compatibilité du polymorphisme de constantes avec les sections.	herbelin	2006-10-29
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28