coq - The formal proof system

Age	Commit message (Expand)	Author
2019-01-21	Refactor typechecking of inductive types	Gaëtan Gilbert
2019-01-21	Move inductive typecheck to file independent from positivity check.	Gaëtan Gilbert
2019-01-21	Move inductive_error to Type_errors	Gaëtan Gilbert
2018-11-26	Put -indices-matter in typing_flags	Gaëtan Gilbert
2018-11-06	[checker] Refactor by sharing code with the kernel	Maxime Dénès
2018-07-24	Projections use index representation	Gaëtan Gilbert
2018-06-23	Adapt the kernel to generate proper data for mutual records.	Pierre-Marie Pédrot
2018-06-17	Remove the proj_body field from the kernel.	Pierre-Marie Pédrot
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
2017-11-06	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-11	CLEANUP: kernel/context.ml{,i}	Matej Kosik
2015-07-09	Kernel: primitive projections handling of let-ins	Matthieu Sozeau
2015-01-12	Update headers.	Maxime Dénès
2014-10-11	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau
2014-08-29	Add test-suite file. Compute the name for the record binder in the	Matthieu Sozeau
2014-08-28	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-05	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey
2013-08-04	Fixing #2846: Uncaught exception Reduction.NotArity.	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-08-08	Updating headers.	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-05-18	Applicative commutative cuts in Fixpoint guard condition	pboutill
2010-04-29	Various minor improvements of comments in mli for ocamldoc	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2009-01-11	- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).	herbelin
2008-01-05	Fixed bug 1761 (unexpected anomaly when constructor type has invalid	herbelin
2007-05-17	Nettoyage et standardisation des messages d'erreurs.	herbelin
2005-12-17	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-02-14	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras
2001-11-05	GROS COMMIT:	barras
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras
2001-03-15	entetes	filliatr
2001-02-14	Mise en place d'un système optionnel de discharge immédiat; prise en compte...	herbelin
2000-12-15	- suppression mind_extract_params	filliatr
2000-12-14	Les params d'inductif deviennent en même temps propre à chaque inductif d'u...	herbelin
2000-12-12	syntaxe AST Inversion + commentaires ocamlweb autour de $	filliatr
2000-10-18	Simplifications autour de typed_type (renommé types par analogie avec sorts)...	herbelin
2000-07-24	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin
2000-06-01	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin
2000-05-31	Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs	herbelin
2000-05-22	Suite restructuration inductifs; changement nom module Constant en Declarations	herbelin