coq - The formal proof system

Age	Commit message (Expand)	Author
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-08	Ensure that template parameters are shared in the same inductive block.	Pierre-Marie Pédrot
2020-02-14	Use thunks to univ instead of lazy constr for template typing	Gaëtan Gilbert
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-27	mind_kelim is the highest allowed sort instead of a list	Gaëtan Gilbert
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-28	Constructor type information uses the expanded form.	Pierre-Marie Pédrot
2018-06-27	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-12-09	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias
2017-11-26	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias
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-06-18	Moving the typing_flags to the environment.	Pierre-Marie Pédrot
2016-06-16	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot
2016-06-14	Assume totality: dedicated type rather than bool	Arnaud Spiwack
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-06-26	Add a flag to deactivate guard checking in the kernel.	Arnaud Spiwack
2015-01-18	Make native compiler handle universe polymorphic definitions.	Maxime Dénès
2015-01-17	Make native compiler handle universe polymorphic definitions.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2014-08-28	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau
2014-08-25	"allows to", like "allowing to", is improper	Jason Gross
2014-08-03	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau
2014-08-01	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin
2014-07-22	Refining match subterm and commutative cut rules. The parameters that are	Maxime Dénès
2014-06-04	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau
2014-05-06	Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.	Matthieu Sozeau
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
2013-05-14	Delayed the computation of parameters in sort polymorphism of	herbelin
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-08-08	Updating headers.	herbelin
2011-07-04	Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml	letouzey
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-06-14	Added printing of recursive notations in cases pattern (supported by wish 2248).	herbelin
2010-05-18	Some ocamldoc comments + Fixing name of .coqrc.version file in refman	pboutill
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
2010-03-11	introduced lazy computation of size info in the guard condition	barras
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-07-15	- Fixing bug #2139 (kernel-based test of well-formation of elimination	herbelin