coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-04-15	[proofs] Move pfedit to `proofs`	Emilio Jesus Gallego Arias
	It seems to belong there, not in `tactics`
2020-04-15	[proof] Move proof_global functionality to Proof_global from Pfedit	Emilio Jesus Gallego Arias
	This actually gets `Pfedit` out of the dependency picture [can be almost merged with `Proof` now, as it is what it manipulates] and would allow to reduce the exported low-level API from `Proof_global`, as `map_fold_proof` is not used anymore.
2020-03-19	[pfedit] Labelize sign parameter	Emilio Jesus Gallego Arias

2020-03-19	[declare] Remaining bits on the consistency of UState.t naming	Emilio Jesus Gallego Arias

2020-03-19	[declare] Remove one use of inline_private_constants	Emilio Jesus Gallego Arias
	We instead favor the `build_by_tactic` function which should at some point better integrated in the declare core.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-10-30	Merge PR #10681: [declare] Make `proof_entry` a private type.	Pierre-Marie Pédrot

2019-10-29	Show diffs in "Show Proof."	Jim Fehrle
	Add experimental "Show Proof" command to the toplevel that shadows the current command in the parser (in coqtop and PG only). Apply existing code to highlight diffs in the output
2019-10-29	[declare] Make `proof_entry` a private type.	Emilio Jesus Gallego Arias
	Proof entries are low-level objects and should not be manipulated by users directly, in particular as we want to unify all the code around declaration of constants. This patch doesn't bring by itself a lot of improvement, other than setting the base where to extend the interface, however it already points out some points of interest, and in particular the manipulation of opacity done by `Derive` which can be quite problematic, and of course the handling of delayed proofs. So while this is a first step, IMHO it doesn't harm a lot having it in place, but a lot more work will be needed, in particular regarding the handling of delayed proofs. To make `proof_entry` a fully abstract type, the remaining work is focused on `abstract` and obligations, both of which do quite a few hackery that will have to be migrated to the `Declare` API.
2019-08-27	[declare] Move proof_entry type to declare, put interactive proof data on ↵	Emilio Jesus Gallego Arias
	top of declare. This PR is a follow up to #10406 , moving the then introduced `proof_entry` type to `Declare`. This makes sense as `Declare` is the main consumer of the entry type, and already provides the constructors for it. This is a step towards making the entry type private, which will allow us to enforce / handle invariants on entry data better. A side-effect of this PR is that now `Proof_global` does depend on `Declare`, not the other way around, but that makes sense given that closing an interactive proof will be a client of declare. Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into tactics due to `abstract`, at some point we may be able to unify all them into a single file in `vernac`.