coq - The formal proof system

Age	Commit message (Expand)	Author
2020-04-13	Partial import inductive(..)	Gaëtan Gilbert
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
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-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-01-20	Update copyright headers.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
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-04-29	Splitting Term into five unrelated interfaces:	ppedrot