Merge PR#481: [option] Remove support for non-synchronous options.

1 files changed, 7 insertions, 0 deletions

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 527721f8a4..a2ae8254db 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -101,6 +101,13 @@ type 'a ast = private {
   implemented in the whole code base. Matching a located object hasn't
   changed, however, `Loc.tag ?loc obj` must be used to build one.
 
+In GOption:
+
+  Support for non-synchronous options has been removed. Now all
+  options are handled as a piece of normal document state, and thus
+  passed to workers, etc... As a consequence, the field
+  `Goptions.optsync` has been removed.
+
 ** Tactic API **
 
 - pf_constr_of_global now returns a tactic instead of taking a continuation.