diff options
Diffstat (limited to 'dev/doc/changes.txt')
| -rw-r--r-- | dev/doc/changes.txt | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 159be9a582..0f1a28028c 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,4 +1,28 @@ ========================================= += CHANGES BETWEEN COQ V8.7 AND COQ V8.8 = +========================================= + +* ML API * + +We removed the following functions: + +- Universes.unsafe_constr_of_global: use Global.constr_of_global_in_context + instead. The returned term contains De Bruijn universe variables. If you don't + depend on universes being instantiated, simply drop the context. +- Universes.unsafe_type_of_global: same as above with + Global.type_of_global_in_context + +We changed the type of the following functions: + +- Global.body_of_constant_body: now also returns the abstract universe context. + The returned term contains De Bruijn universe variables. +- Global.body_of_constant: same as above. + +We renamed the following datatypes: + + Pp.std_ppcmds -> Pp.t + +========================================= = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = ========================================= @@ -8,6 +32,16 @@ Coq is compiled with -safe-string enabled and requires plugins to do the same. This means that code using `String` in an imperative way will fail to compile now. They should switch to `Bytes.t` +* Plugin API * + +Coq 8.7 offers a new module overlay containing a proposed plugin API +in `API/API.ml`; this overlay is enabled by adding the `-open API` +flag to the OCaml compiler; this happens automatically for +developments in the `plugin` folder and `coq_makefile`. + +However, `coq_makefile` can be instructed not to enable this flag by +passing `-bypass-API`. + * ML API * Added two functions for declaring hooks to be executed in reduction @@ -154,6 +188,9 @@ In Coqlib / reference location: - The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase was very specific. Use tclPROGRESS instead. +- New (internal) tactical `tclINDEPENDENTL` that combined with enter_one allows + to iterate a non-unit tactic on all goals and access their returned values. + - The unsafe flag of the Refine.refine function and its variants has been renamed and dualized into typecheck and has been made mandatory. |