diff options
Diffstat (limited to 'dev/doc/changes.md')
| -rw-r--r-- | dev/doc/changes.md | 32 |
1 files changed, 30 insertions, 2 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 7221c3de56..51d90df89f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -5,6 +5,21 @@ - Functions and types deprecated in 8.10 have been removed in Coq 8.11. +- Type Decl_kinds.locality has been restructured, see commit + 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 @@ -59,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 @@ -1278,7 +1306,7 @@ next_global_ident_away true -> next_ident_away_in_goal next_global_ident_away false -> next_global_ident_away ``` -### Cleaning in commmand.ml +### Cleaning in command.ml Functions about starting/ending a lemma are in lemmas.ml Functions about inductive schemes are in indschemes.ml @@ -1593,7 +1621,7 @@ Other kinds of objects: #### Writing subst_thing functions -The subst_thing shoud not copy the thing if it hasn't actually +The subst_thing should not copy the thing if it hasn't actually changed. There are some cool emacs macros in dev/objects.el to help writing subst functions this way quickly and without errors. Also there are *_smartmap functions in Util. |