coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-16	Infrastructure for cumulative inductive syntax (no grammar extension yet)	Gaëtan Gilbert
2020-10-21	Deprecate the non-qualified equality functions on kerpairs.	Pierre-Marie Pédrot
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-04-16	Checker: factorize handling of typing flags	Gaëtan Gilbert
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-03-08	Template polymorphism is now a property of the inductive block.	Pierre-Marie Pédrot
2020-02-09	Remove the Template Check option.	Pierre-Marie Pédrot
2020-02-05	Remove a dubious part of the checker code relying on a universe context	Pierre-Marie Pédrot
2020-02-05	Store the template polymorphic context inside the TemplateArity node.	Pierre-Marie Pédrot
2020-01-27	Checker: use inductive's check_template flag	Gaëtan Gilbert
2020-01-15	Discharge inductive types without rechecking them	Gaëtan Gilbert
2020-01-15	generate variance data for section universes (not yet used)	Gaëtan Gilbert
2019-12-16	Remove variance info from inductive entries, infer in indtyping	Gaëtan Gilbert
2019-08-16	Fix typing_flags in the checker	SimonBoulier
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	Repair relevance marks in-kernel.	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
2019-02-17	Separate variance and universe fields in inductives.	Gaëtan Gilbert
2018-12-19	coqchk: fix check for kelim with functors	Gaëtan Gilbert
2018-12-12	checker: check inductive types by roundtrip through the kernel.	Gaëtan Gilbert
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-06	[checker] Fix "error related to inductive types"	Maxime Dénès
2018-11-06	[checker] Refactor by sharing code with the kernel	Maxime Dénès