From 7dba9d3f3ce62246b9d8562d2818c63ba37b206e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 21 Jul 2014 10:03:04 +0200
Subject: STM: new "par:" goal selector, like "all:" but in parallel

par: distributes the goals among a number of workers given
by -async-proofs-tac-j (defaults to 2).
---
 lib/flags.ml  | 1 +
 lib/flags.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index 4b323f611b..75f149eb69 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -51,6 +51,7 @@ let compilation_mode = ref BuildVo
 type async_proofs = APoff | APonLazy | APon
 let async_proofs_mode = ref APoff
 let async_proofs_n_workers = ref 1
+let async_proofs_n_tacworkers = ref 2
 let async_proofs_private_flags = ref None
 let async_proofs_always_delegate = ref false
 let async_proofs_never_reopen_branch = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index db1d8bcc46..4697e4cacd 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -18,6 +18,7 @@ val compilation_mode : compilation_mode ref
 type async_proofs = APoff | APonLazy | APon
 val async_proofs_mode : async_proofs ref
 val async_proofs_n_workers : int ref
+val async_proofs_n_tacworkers : int ref
 val async_proofs_private_flags : string option ref
 val async_proofs_is_worker : unit -> bool
 val async_proofs_is_master : unit -> bool
-- 
cgit v1.2.3