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.
2019-02-12	[tactics] Remove dependency of abstract on global proof state.	Emilio Jesus Gallego Arias
	In order to do so we place the polymorphic status and name in the read-only part of the monad. Note the added comments, as well as the fact that almost no part of tactics depends on `proofs` nor `interp`, thus they should be placed just after pretyping. Gaëtan Gilbert noted that ideally, abstract should not depend on the polymorphic status, should we be able to defer closing of the constant, however this will require significant effort. Also, we may deprecate nameless abstract, thus rending both of the changes this PR need unnecessary.
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-09	Adding universe names to polymorphic entry instances.	Pierre-Marie Pédrot

2018-10-30	Move abstract out of tactics.ml	Gaëtan Gilbert