coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-06-26	[declare] Move proof information to declare.	Emilio Jesus Gallego Arias
	At this point the record in lemmas was just a stub; next commit will stop exposing the internals of mutual information, and pave the way for the refactoring of `Info.t` handling in the Declare interface.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-06-09	[proof] Move proofs that have an associated constant to `Lemmas`	Emilio Jesus Gallego Arias
	The main idea of this PR is to distinguish the types of "proof object" `Proof_global.t` and the type of "proof object associated to a constant, the new `Lemmas.t`. This way, we can move the terminator setup to the higher layer in `vernac`, which is the one that really knows about constants, paving the way for further simplification and in particular for a unified handling of constant saving by removal of the control inversion here. Terminators are now internal to `Lemmas`, as it is the only part of the code applying them. As a consequence, proof nesting is now handled by `Lemmas`, and `Proof_global.t` is just a single `Proof.t` plus some environmental meta-data. We are also enable considerable simplification in a future PR, as this patch makes `Proof.t` and `Proof_global.t` essentially the same, so we should expect to handle them under a unified interface.
2019-03-27	[plugins] [derive] Adapt to removal of imperative proof state.	Emilio Jesus Gallego Arias

2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-06-07	Put all plugins behind an "API".	Matej Kosik

2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2015-01-08	Avoiding introducing yet another convention in naming files.	Hugo Herbelin