coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-04-13	Fix #11783 Require in Section	Gaëtan Gilbert

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-01-15	generate variance data for section universes (not yet used)	Gaëtan Gilbert
	preparation for direct discharge
2019-12-07	Section.t is never empty	Gaëtan Gilbert
	This approach using `type t = { sec_prev: t option; sec_... }` makes it easy to update sections using the record update syntax, but impossible to statically ensure that an operation only affects the current section. We may instead consider using `type t = section * section list` which needs some boilerplate to update.
2019-10-14	Use kernel info from Global for Lib.sections_{depth,are_opened}	Gaëtan Gilbert

2019-10-05	Remove "is_polymorphic_univ" checks in upper layers.	Gaëtan Gilbert
	There were 2: - when declaring a constraint to avoid monomorphic constraint referring to polymorphic univs, this check is redundant with the check in Section.ml - when declaring a universe context to avoid redeclaring universes, this is not necessary after recent commits.
2019-10-02	Loosen restrictions on mixing universe mono/polymorphism in sections	Gaëtan Gilbert
	We disallow adding univ constraints wich refer to polymorphic universes, and monomorphic constants and inductives when polymorphic universes or constraints are present. Every other combination is already correctly discharged by the kernel.
2019-09-26	Implement section discharging inside kernel.	Pierre-Marie Pédrot
	This patch is minimalistic, insofar as it is only untying the dependency loop between Declare and Safe_typing. Nonetheless, it is already quite big, thus we will polish it afterwards.
2019-09-25	Move the Lib section data into the kernel.	Pierre-Marie Pédrot
	Due to the redundancy with some other declaration-specific data from the kernel, we also seize the opportunity to clean it up. Note also that discharging is still performed outside of the kernel for now.