diff options
Diffstat (limited to 'dev/doc/changes.md')
| -rw-r--r-- | dev/doc/changes.md | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index cc58222fbf..51d90df89f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -9,6 +9,17 @@ message. Main change to do generally is to change the flag "Global" to "Global ImportDefaultBehavior". +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. + + 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. + ## Changes between Coq 8.9 and Coq 8.10 ### ML4 Pre Processing @@ -63,6 +74,19 @@ Coqlib: command then enables to locate the registered constant through its name. The name resolution is dynamic. +Proof state: + +- Handling of proof state has been fully functionalized, thus it is + not possible to call global functions such as `get_current_context ()`. + + The main type for functions that need to handle proof state is + `Proof_global.t`. + + Unfortunately, this change was not possible to do in a + backwards-compatible way, but in most case the api changes are + straightforward, with functions taking and returning an extra + argument. + Macros: - The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are |