diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-11 11:27:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-10-11 11:27:15 +0200 |
| commit | 16dec9697b06a7fbda0997ab0685ef24443c7d3a (patch) | |
| tree | 1f85ee8f06535198d402ef9879883f3225291e6b /lib/flags.mli | |
| parent | 35c36f80dcc1e61e3dae8bcce1da71b384904582 (diff) | |
[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)
We move delicate library/module instillation code to the STM so the
API guarantees that the first state snapshot is correct. That was not
the case in the past, which meant that the STM cache was unsound in
batch mode, however we never used its contents due to not backtracking
to the first state.
This provides quite an improvement in the API, however more work is
needed until the codepath is fully polished.
This is a critical step towards handling the STM functionally.
Diffstat (limited to 'lib/flags.mli')
| -rw-r--r-- | lib/flags.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/flags.mli b/lib/flags.mli index 8ec2a8073..5233e72a2 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -11,7 +11,6 @@ (** Command-line flags *) val boot : bool ref -val load_init : bool ref (** Set by coqtop to tell the kernel to output to the aux file; will be eventually removed by cleanups such as PR#1103 *) |