From 42cbdfccf0c0500935d619dccaa00476690229f8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 17 Jun 2016 16:24:37 +0200
Subject: par: like all: but in parallel

This commit documents par:, fixes its semantics so that is
behaves like all:, supports (toplevel) abstract and optimizes
toplevel solve.

`par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1`
but is optimized for failures: if one goal fails all are aborted
immediately.

`par: abstract tac` runs abstract on the generated proof terms.  Nested
abstract calls are not supported.
---
 intf/vernacexpr.mli | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 45d71e32bb..1c75d76dd5 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -484,9 +484,11 @@ and opacity_guarantee =
   | GuaranteesOpacity (** Only generates opaque terms at [Qed] *)
   | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*)
 and proof_step = { (* TODO: inline with OCaml 4.03 *)
-  parallel : bool;
+  parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
   proof_block_detection : proof_block_name option
 }
+and solving_tac = bool (* a terminator *)
+and anon_abstracting_tac = bool (* abstracting anonymously its result *)
 and proof_block_name = string (* open type of delimiters *)
 type vernac_when =
   | VtNow
-- 
cgit v1.2.3