coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Correction de 2 bugs critiques du polymorphisme d'univers	herbelin	2006-10-27
*	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin	2006-10-05
*	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir	2006-07-22
*	Correction bug du polymorphisme de sort des inductifs (cas où les variables ...	herbelin	2006-06-22
*	- Indtypes: en attente opinion CoRN, les occurrences de Type non explicites	herbelin	2006-05-28
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	correction bugs de condition de garde (fix + cofix)	barras	2006-05-12
*	subst. explicites avec vecteurs	barras	2006-05-09
*	fixed bug #804: removed useless reduction in fix guard checking	barras	2006-05-03
*	Inductifs avec polymorphisme de sorte (version initiale)	herbelin	2006-03-29
*	- Correction bug calcul mind_consnrealargs, introduit à la révision	herbelin	2006-03-22