coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had	Pierre-Marie Pédrot	2014-03-14
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Removing useless casts between arrays and lists.	ppedrot	2013-08-04
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey	2013-03-13
*	Term.dest* functions now raise specific DestKO exn instead of Invalid_argument	letouzey	2013-03-12
*	More informative error when a global reference is used in a context of	herbelin	2013-02-28
*	Modulification of identifier	ppedrot	2012-12-14
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	Fixing vm_compute bug #2729 (function used to decompose constructors	herbelin	2012-03-13
*	fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...	barras	2010-07-29
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Correcting a delta normalization bug in VM (checked by benjamin)	jforest	2008-09-30
*	fixed bug #1780: a lift was missing (match predicate)	barras	2008-05-29
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
*	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack	2007-12-18
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
*	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin	2007-01-19
*	correction du bug : VM value extraction error (PR#1290)	bgregoir	2006-11-29
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir	2006-07-22