coq - The formal proof system

Age	Commit message (Expand)	Author
2019-05-14	Abstract away the implementation of side-effects in Safe_typing.	Pierre-Marie Pédrot
2019-02-17	Separate variance and universe fields in inductives.	Gaëtan Gilbert
2019-02-04	Primitive integers	Maxime Dénès
2018-11-09	Use arrays of names instead of lists in abstract universe names.	Pierre-Marie Pédrot
2018-11-09	Adding universe names to polymorphic entry instances.	Pierre-Marie Pédrot
2018-10-26	Remove a few circumvolutions around parameters of inductive entries	Maxime Dénès
2018-09-03	Merge PR #7912: Simplify effects API	Maxime Dénès
2018-06-27	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin
2018-06-24	Further cleaning of the side-effect API.	Pierre-Marie Pédrot
2018-06-24	Share the role type between the implementations of side-effects.	Pierre-Marie Pédrot
2018-06-23	Using more general information for primitive records.	Pierre-Marie Pédrot
2018-06-17	Remove special declaration of primitive projections in the kernel.	Pierre-Marie Pédrot
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-12-19	Let definitions do not create new universe constraints.	Pierre-Marie Pédrot
2017-12-19	Specific type for section definition entries.	Pierre-Marie Pédrot
2017-12-10	[api] Remove kernel dependency on intf (Decl_kind)	Emilio Jesus Gallego Arias
2017-11-24	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert
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-26	More precise type for universe entries.	Pierre-Marie Pédrot
2017-07-25	[api] Put modules in order in API.{mli,ml}	Emilio Jesus Gallego Arias
2012-10-23	Cleared a purely declarative .ml file and moved its interface to intf/	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-08-08	Updating headers.	herbelin
2011-12-12	Proof using ...	gareuselesinge
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-01-31	A fine-grain control of inlining at functor application via priority levels	letouzey
2011-01-28	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-10-21	This big commit addresses two problems:	soubiran
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-04-08	Some dead code removal + cleanups	letouzey
2008-03-14	Ajout des alias de module dans le noyau.	soubiran
2008-02-01	Beaoucoup de changements dans la representation interne des modules.	soubiran
2007-04-25	New keyword "Inline" for Parameters and Axioms for automatic	soubiran
2007-02-21	Removed some useless code in mod_typing that was redundant with safe_typing.	soubiran
2006-03-18	MAJ documentation en syntaxe v8	herbelin
2005-11-02	Types inductifs parametriques	mohring
2005-01-13	Construct "T with (Definition\|Module) id := c" generalized to	sacerdot
2004-10-20	COMMITED BYTECODE COMPILER	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-06-25	correspondance des records et noms de champs de records entre un module et sa...	letouzey
2002-08-19	La notation 'with'. L'interpretation - version preliminaire	coq
2002-08-02	Modules dans COQ\!\!\!\!	coq