From 16dec9697b06a7fbda0997ab0685ef24443c7d3a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 11 Oct 2017 11:27:15 +0200 Subject: [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. --- lib/flags.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'lib/flags.mli') 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 *) -- cgit v1.2.3