coq - The formal proof system

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