coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-08-29	[funind] Don't export duplicate save function.	Emilio Jesus Gallego Arias
	It will take a bit more to clean up the mess with entries in the `indfun` plugin [quite a few PRs in the queue], but thanks to recent refactoring the tricky parts are self-contained now in `gen_principle` so we can remove the duplicated `save` function from the public API.
2019-08-27	[declare] Use entry constructor instead of low-level record.	Emilio Jesus Gallego Arias
	Non-delayed entries can be done with the current constructor, delayed ones will require more work.
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`.
2019-08-27	Merge PR #10635: [funind] Port indfun to the new tactic engine.	Pierre-Marie Pédrot
	Reviewed-by: ppedrot
2019-08-23	[lemmas] Cleanup users of default proof information.	Emilio Jesus Gallego Arias
	We remove calls of `Lemmas.Info.make` that where using the default parameters, as this is mostly dead code now. This brings into question quite a few things, in particular, the uneven support of `scope` attributes by different commands / plugins. We don't attempt to solve that yet, hopefully the ongoing constant saving path refactoring will be able to take care of these inconsistencies.
2019-08-19	[api] Move handling of variable implicit data to impargs	Emilio Jesus Gallego Arias
	We move `binder_kind` to the pretyping AST, removing the last data type in the now orphaned file `Decl_kinds`. This seems a better fit, as this data is not relevant to the lower layers but only used in `Impargs`. We also move state keeping to `Impargs`, so now implicit declaration must include the type. We also remove a duplicated function.
2019-08-07	[funind] Move some exception-based control flow to explicit option typing.	Emilio Jesus Gallego Arias

2019-07-31	[funind] Remove export of `generate_functional_principle` and `make_scheme`	Emilio Jesus Gallego Arias
	This removes the export of two internal functions, moving to their only use place. In particular, `make_scheme` was exposing the low-level `proof_entry` object, which should not do. This will allow to refactor all these constant-building functions towards a more uniform use of the API. In particular, all the functions manipulating proof entries directly are in `Gen_principle`.
2019-07-31	[funind] Move duplicated `observe_tac` function to indfun_common.	Emilio Jesus Gallego Arias
	We also attempt a version that may work with `Proofview.tactic` , may need more work.
2019-07-31	[funind] Move common `make_eq` to funind_common.	Emilio Jesus Gallego Arias

2019-07-31	[funind] Move principle generation to its own file.	Emilio Jesus Gallego Arias