diff options
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/changes.txt | 7 |
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. |