aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/flags.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-09-16 16:57:59 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-09-16 17:34:57 +0200
commit4dc8746cac24ba72a1ec4dfa764a1ae88ce79277 (patch)
tree2987141c16e3ec03afc1d3b11cb3d7b3334c6580 /lib/flags.mli
parent26aa224293e88611dcb543e400488013bc8b30b4 (diff)
Undo prints only if coqtop || emacs
Diffstat (limited to 'lib/flags.mli')
-rw-r--r--lib/flags.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/flags.mli b/lib/flags.mli
index 98f0acb95..f94d80ffc 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -17,6 +17,8 @@ val compilation_mode : compilation_mode ref
type async_proofs = APoff | APonLazy | APon
val async_proofs_mode : async_proofs ref
+type cache = Force
+val async_proofs_cache : cache option ref
val async_proofs_n_workers : int ref
val async_proofs_n_tacworkers : int ref
val async_proofs_private_flags : string option ref