aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/flags.ml
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.ml
parent26aa224293e88611dcb543e400488013bc8b30b4 (diff)
Undo prints only if coqtop || emacs
Diffstat (limited to 'lib/flags.ml')
-rw-r--r--lib/flags.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 2bc217fa3..0356863ab 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -50,6 +50,8 @@ let compilation_mode = ref BuildVo
type async_proofs = APoff | APonLazy | APon
let async_proofs_mode = ref APoff
+type cache = Force
+let async_proofs_cache = ref None
let async_proofs_n_workers = ref 1
let async_proofs_n_tacworkers = ref 2
let async_proofs_private_flags = ref None