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).
---
 proofs/pfedit.ml       | 2 ++
 proofs/proof_global.ml | 1 +
 2 files changed, 3 insertions(+)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 0c4250535b..49195aecce 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -95,6 +95,8 @@ let solve ?with_end_tac gi tac pr =
     let tac = match gi with
       | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
       | Vernacexpr.SelectAll -> tac
+      | Vernacexpr.SelectAllParallel ->
+          Errors.anomaly(str"SelectAllParallel not handled by Stm")
     in
     Proof.run_tactic (Global.env ()) tac pr
   with
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f10b07da3f..96bc265fc2 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -529,6 +529,7 @@ let get_default_goal_selector () = !default_goal_selector
 let print_goal_selector = function
   | Vernacexpr.SelectAll -> "all"
   | Vernacexpr.SelectNth i -> string_of_int i
+  | Vernacexpr.SelectAllParallel -> "par"
 
 let parse_goal_selector = function
   | "all" -> Vernacexpr.SelectAll
-- 
cgit v1.2.3