diff options
| author | Maxime Dénès | 2018-02-06 14:15:19 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-06 14:15:19 +0100 |
| commit | b1d56e48b2453814a5d2898688fbc7c5d29d32fa (patch) | |
| tree | 4fc10644e5db337a6d931ad1a26974a34399b97e /dev | |
| parent | 5ac5ba83b7527f29b6a00c51806d4842b2e22e44 (diff) | |
| parent | c13213ced52f8f1383d5bed9c5a826d111603318 (diff) | |
Merge PR #6671: [stm] [toplevel] Make loadpath a parameter of the document.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.md | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index e616bd5663..aef62b0092 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -58,6 +58,17 @@ 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". +### STM API + +The STM API has seen a general overhaul. The main change is the +introduction of a "Coq document" type, which all operations now take +as a parameter. This effectively functionalize the STM API and will +allow in the future to handle several documents simultaneously. + +The main remarkable point is that key implicit global parameters such +as load-paths and required modules are now arguments to the document +creation function. This helps enforcing some key invariants. + ### XML IDE Protocol - Before 8.8, `Query` only executed the first command present in the |