coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-03-14	Repair relevance marks in-kernel.	Gaëtan Gilbert
	Prevent errors when under annotating binders.
2019-03-14	Inductives in SProp, forbid primitive records with only sprop fields	Gaëtan Gilbert
	For nonsquashed: Either - 0 constructors - primitive record
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
	Kernel should be mostly correct, higher levels do random stuff at times.
2019-03-14	Add a non-cumulative impredicative universe SProp.	Gaëtan Gilbert
	Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged.
2019-02-17	Separate variance and universe fields in inductives.	Gaëtan Gilbert
	I think the usage looks cleaner this way.
2019-01-21	Refactor typechecking of inductive types	Gaëtan Gilbert
	We split into smaller functions, use more specific types for universe manipulation, and try to limit how much of the big tuple gets passed to subroutines.
2019-01-21	Move inductive typecheck to file independent from positivity check.	Gaëtan Gilbert
	This is strictly code movement.