coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-05-18	Cleanup: remove noisy "sec_" prefixes in section.ml	Gaëtan Gilbert

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-04	Remove redundancy in section hypotheses of kernel entries.	Pierre-Marie Pédrot
	We only do it for entries and not declarations because the upper layers rely on the kernel being able to quickly tell that a definition is improperly used inside a section. Typically, tactics can mess with the named context and thus make the use of section definitions illegal. This cannot happen in the kernel but we cannot remove it due to the code dependency. Probably fixing a soundness bug reachable via ML code only. We were doing fancy things w.r.t. computation of the transitive closure of the the variables, in particular lack of proper sanitization of the kernel input.
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.