coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-07-03	Remove unused variable_path (note secpath is still used)	Gaëtan Gilbert

2019-07-03	declare_variable: path is always Lib.cwd()	Gaëtan Gilbert

2019-07-03	Remove unused Decls.variable_{context,polymorphic}	Gaëtan Gilbert

2019-07-01	[decls] Remove goal_object_kind type.	Emilio Jesus Gallego Arias
	We can use logical kind for the same purpose, which is mainly dumpglob, so `goal_object_kind` was never matched against, making this transformation safe.
2019-07-01	[dumpglob] Move dumpglob-specific data to dumpglob.	Emilio Jesus Gallego Arias
	The whole business of cst_kind is fishy tho, it seems to me that it should be removed from the libobject path.
2019-07-01	[api] Refactor most of `Decl_kinds`	Emilio Jesus Gallego Arias
	We move the bulk of `Decl_kinds` to a better place [namely `interp/decls`] and refactor the use of this information quite a bit. The information seems to be used almost only for `Dumpglob`, so it certainly should end there to achieve a cleaner core. Note the previous commits, as well as the annotations regarding the dubious use of the "variable" data managed by the `Decls` file. IMO this needs more work, but this should be a good start.