coq - The formal proof system

Age	Commit message (Expand)	Author
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-05-13	Make explicit that UGraph lower bounds are only of two kinds.	Pierre-Marie Pédrot
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-03-08	Do not hardcode specific handling of Prop levels in template poly.	Pierre-Marie Pédrot
2020-02-09	Remove the Template Check option.	Pierre-Marie Pédrot
2020-02-07	Merge PR #11528: Checker does not rely on Monomorphic fields	Gaëtan Gilbert
2020-02-05	Store the template polymorphic context inside the TemplateArity node.	Pierre-Marie Pédrot
2020-01-29	Nicer kernel universe error for inductives	Gaëtan Gilbert
2020-01-15	generate variance data for section universes (not yet used)	Gaëtan Gilbert
2020-01-14	infercumulativity: take less arguments	Gaëtan Gilbert
2020-01-07	minor cleanup template_polymorphic_univs: check_levels returns bool	Gaëtan Gilbert
2019-12-18	Merge PR #10616: Fix push_universe_context* interfaces to use a consistent ~s...	Pierre-Marie Pédrot
2019-12-16	Remove variance info from inductive entries, infer in indtyping	Gaëtan Gilbert
2019-12-13	Use ~strict argument consistently in push_context/push_context_set intfs	Matthieu Sozeau
2019-11-26	indTyping: error instead of anomaly for ill-formed template	Gaëtan Gilbert
2019-11-26	Fix #11039: proof of False with template poly and nonlinear universes	Gaëtan Gilbert
2019-08-26	Make kernel parametric on the lowest universe and fix #9294	Matthieu Sozeau
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	Inductives in SProp, forbid primitive records with only sprop fields	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-02-17	Separate variance and universe fields in inductives.	Gaëtan Gilbert
2019-01-21	Refactor typechecking of inductive types	Gaëtan Gilbert
2019-01-21	Move inductive typecheck to file independent from positivity check.	Gaëtan Gilbert