diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.md | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 51d90df89f..ab9df12766 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -13,13 +13,31 @@ Proof state: Proofs that are attached to a top-level constant (such as lemmas) are represented by `Lemmas.t`, as they do contain additional - information related to the constant declaration. + information related to the constant declaration. Some functions have + been renamed from `start_proof` to `start_lemma` + Plugins that require access to the information about currently opened lemmas can add one of the `![proof]` attributes to their `mlg` entry, which will refine the type accordingly. See documentation in `vernacentries` for more information. + Proof `terminators` have been removed in favor of a principled + proof-saving path. This should not affect the regular API user, but + if plugin writes need special handling of the proof term they should + now work with Coq upstream to unsure the provided API does work and + is principled. Closing `hooks` are still available for simple + registration on constant save path, and essentially they do provide + the same power as terminators, but don't encourage their use other + than for simple tasks [such as adding a constant to a database] + + Additionally, the API for proof/lemma handling has been refactored, + triples have been split into named arguments, and a few bits of + duplicated information among layers has been cleaned up. Most proof + information is now represented in a direct-style, as opposed to it + living inside closures in previous Coq versions; thus, proof + manipulation possibilities have been improved. + ## Changes between Coq 8.9 and Coq 8.10 ### ML4 Pre Processing |