coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-02-17	Separate variance and universe fields in inductives.	Gaëtan Gilbert
	I think the usage looks cleaner this way.
2018-12-19	coqchk: fix check for kelim with functors	Gaëtan Gilbert

2018-12-12	checker: check inductive types by roundtrip through the kernel.	Gaëtan Gilbert

2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
	This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :)
2018-11-06	[checker] Fix "error related to inductive types"	Maxime Dénès

2018-11-06	[checker] Refactor by sharing code with the kernel	Maxime Dénès
	For historical reasons, the checker was duplicating a lot of code of the kernel. The main differences I found were bug fixes that had not been backported. With this patch, the checker uses the kernel as a library to serve the same purpose as before: validation of a `.vo` file, re-typechecking all definitions a posteriori. We also rename some files from the checker so that they don't clash with kernel files.