From ce2b2058587224ade9261cd4127ef4f6e94d356b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 27 Feb 2017 20:16:40 +0100
Subject: [stm] Port the toplevel to the STM.

- We clean-up `Vernac` and make it use the STM API.

- Now functions in `Vernac` for use in the toplevel and compiler take
  an starting `Stateid.t`.

- Duplicated `Stm.interp` entry point is removed.

- The XML protocol call `interp` is disabled.
---
 dev/doc/changes.txt | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'dev/doc')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 30edea7f2f..7e7bb98580 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -156,6 +156,19 @@ document type". This allows for a more uniform handling of printing
 
 - A few unused hooks were removed due to cleanups, no clients known.
 
+** Toplevel and Vernacular API **
+
+- The components related to vernacular interpretation have been moved
+  to their own folder `vernac/` whereas toplevel now contains the
+  proper toplevel shell and compiler.
+
+- Coq's toplevel has been ported to directly use the common `Stm`
+  API. The signature of a few functions has changed as a result.
+
+** XML Protocol **
+
+- The legacy `interp` call has been turned into a noop.
+
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
-- 
cgit v1.2.3