diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-07-19 15:31:29 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-07-19 15:31:29 +0200 |
| commit | e273ff57ef82e81ab6b6309584a7d496ae4659c1 (patch) | |
| tree | 19dc62a48763943e7de049ee3aab515503038339 /dev | |
| parent | 28b3bfd84718e5b29f8e3452fcfe22b19e9910dd (diff) | |
| parent | 6be0e422de395dbdeebb6c481511eb49945eeca8 (diff) | |
Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index c3c86ac5c..57c7a97d5 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -28,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 |