Merge PR #6859: [stm] Make toplevels standalone executables.

1 files changed, 12 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 3030e3311c..aea7ec2f6b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,6 +36,18 @@ Tactic language
   called by OCaml-defined tactics.
 - Option "Ltac Debug" now applies also to terms built using Ltac functions.
 
+Coq binaries and process model
+
+- Before 8.9, Coq distributed a single `coqtop` binary and a set of
+  dynamically loadable plugins that used to take over the main loop
+  for tasks such as IDE language server or parallel proof checking.
+
+  These plugins have been turned into full-fledged binaries so each
+  different process has associated a particular binary now, in
+  particular `coqidetop` is the CoqIDE language server, and
+  `coq{proof,tactic,query}worker` are in charge of task-specific and
+  parallel proof checking.
+
 Changes from 8.8.0 to 8.8.1
 ===========================