diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.txt | 30 | ||||
| -rw-r--r-- | dev/doc/naming-conventions.tex | 2 |
2 files changed, 31 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 159be9a582..57c7a97d58 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -1,4 +1,24 @@ ========================================= += 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. + +========================================= = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = ========================================= @@ -8,6 +28,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 diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex index 349164948d..337b9226df 100644 --- a/dev/doc/naming-conventions.tex +++ b/dev/doc/naming-conventions.tex @@ -267,7 +267,7 @@ If the conclusion is in the other way than listed below, add suffix {forall x y:D, op (op' x y) = op' x (op y)} \itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent} -{forall x:D, op x n = x} +{forall x:D, op x x = x} \itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent} {forall x:D, op (op x) = op x} |