coq - The formal proof system

Age	Commit message (Expand)	Author
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-03-14	Add a non-cumulative impredicative universe SProp.	Gaëtan Gilbert
2019-03-14	Make Sorts.t private	Gaëtan Gilbert
2018-11-06	Move debug term printer to kernel	Maxime Dénès
2018-06-26	Remove Sorts.contents	Gaëtan Gilbert
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-07-04	Bump year in headers.	Pierre-Marie Pédrot
2016-03-22	A patch renaming equal into eq in the module dealing with	Hugo Herbelin
2016-01-20	Update copyright headers.	Maxime Dénès
2015-08-02	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin
2015-08-02	A patch renaming equal into eq in the module dealing with	Hugo Herbelin
2015-06-26	Share prop/set values in sorts.ml.	Matthieu Sozeau
2015-06-26	BUGFIX: Three fixes for the price of 1 in sorts.ml:	Matthieu Sozeau
2015-01-12	Update headers.	Maxime Dénès
2014-12-17	Ensuring the good invariants of hashcons table generation in the API.	Pierre-Marie Pédrot
2014-05-06	Fix extraction taking a type in the wrong environment.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-24	Specializing hash functions for widely used types.	ppedrot
2013-10-23	cList: set-as-list functions are now with an explicit comparison	letouzey
2013-08-22	More complete hashcons : lists (dirpath), arrays (constr)	letouzey
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot