aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc/changes.md
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc/changes.md')
-rw-r--r--dev/doc/changes.md17
1 files changed, 7 insertions, 10 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 01aa6b599..e616bd566 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -12,16 +12,6 @@ All the bugs with a number below 1154 had to be renumbered, you can find
a correspondence table [here](/dev/bugzilla2github_stripped.csv).
All the other bugs kept their number.
-### Plugin API
-
-Coq 8.8 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
General deprecation
@@ -68,6 +58,13 @@ Declaration of printers for arguments used only in vernac command
happen. An alternative is to register the corresponding argument as
a value, using "Geninterp.register_val0 wit None".
+### XML IDE Protocol
+
+- Before 8.8, `Query` only executed the first command present in the
+ `query` string; starting with 8.8, the caller may include several
+ statements. This is useful for instance for temporarily setting an
+ option and then executing a command.
+
## Changes between Coq 8.6 and Coq 8.7
### Ocaml