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.

1 files changed, 18 insertions, 0 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 722249191..5ba3c308a 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -209,6 +209,8 @@ is understood as
 \\
 \selector & ::= &
         [{\ident}]\\
+& $|$ & {\tt all}\\
+& $|$ & {\tt par}\\
 & $|$ & {\integer}\\
 & $|$ & \nelist{{\it (}{\integer} {\it |} {\integer} {\tt -} {\integer}{\it )}}
           {\tt ,}
@@ -393,6 +395,22 @@ all selected goals.
     In this variant, {\tacexpr} is applied globally to the subset
     of goals described by the given ranges. You can write a single
     $n$ as a shortcut for $n$-$n$ when specifying multiple ranges.
+
+  \item {\tt all: } {\tacexpr}
+
+    In this variant, {\tacexpr} is applied to all focused goals.
+
+  \item {\tt par: } {\tacexpr}
+
+    In this variant, {\tacexpr} is applied to all focused goals
+    in parallel.  The number of workers can be controlled via the
+    command line option {\tt -async-proofs-tac-j} taking as argument
+    the desired number of workers.  Limitations:  {\tt par: } only works
+    on goals containing no existential variables and {\tacexpr} must
+    either solve the goal completely or do nothing (i.e. it cannot make
+    some progress).
+    {\tt par: } can only be used at the top level of a tactic expression.
+
 \end{Variants}
 
 \ErrMsg \errindex{No such goal}