aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/control.mli
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-10 04:27:21 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-11 12:43:25 +0100
commit50159f9c1748ccf1d66341d171081a998d116d2f (patch)
treeef58c58b10abcb45142b56d261bc15f034b2731e /lib/control.mli
parenta758aac39aa330911f5f589ab3cae1bebed1e9ce (diff)
[flags] [stm] Reorganize flags.
We move the main async flags to the STM in preparation for more state encapsulation. There is still more work to do, in particular we should make some of the defaults a parameter instead of a flag.
Diffstat (limited to 'lib/control.mli')
-rw-r--r--lib/control.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/control.mli b/lib/control.mli
index f6c63ffb3..261b07693 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -8,6 +8,9 @@
(** Global control of Coq. *)
+(** Will periodically call [Thread.delay] if set to true *)
+val enable_thread_delay : bool ref
+
val interrupt : bool ref
(** Coq interruption: set the following boolean reference to interrupt Coq
(it eventually raises [Break], simulating a Ctrl-C) *)