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.

2 files changed, 45 insertions, 6 deletions

diff --git a/test-suite/success/par_abstract.v b/test-suite/success/par_abstract.v
new file mode 100644
index 0000000000..7f6f9d6279
--- /dev/null
+++ b/test-suite/success/par_abstract.v
@@ -0,0 +1,25 @@
+Axiom T : Type.
+
+Lemma foo : True * Type.
+Proof.
+  split.
+  par: abstract (exact I || exact T).
+Defined.
+
+(* Yes, these names are generated hence
+   the test is fragile.  I want to assert
+   that abstract was correctly handled
+   by par: *)
+Check foo_subproof.
+Check foo_subproof0.
+Check (refl_equal _ :
+  foo =
+  pair foo_subproof foo_subproof0).
+
+Lemma bar : True * Type.
+Proof.
+  split.
+  par: (exact I || exact T).
+Defined.
+Check (refl_equal _ :
+  bar = pair I T).
diff --git a/test-suite/success/paralleltac.v b/test-suite/success/paralleltac.v
index 94ff96ef80..d25fd32a13 100644
--- a/test-suite/success/paralleltac.v
+++ b/test-suite/success/paralleltac.v
@@ -1,3 +1,17 @@
+Lemma test_nofail_like_all1 :
+  True /\ False.
+Proof.
+split.
+all: trivial.
+Admitted.
+
+Lemma test_nofail_like_all2 :
+  True /\ False.
+Proof.
+split.
+par: trivial.
+Admitted.
+
 Fixpoint fib n := match n with
   | O => 1
   | S m => match m with
@@ -19,28 +33,28 @@ Lemma test_old x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T1: linear".
-Time all: solve_P.
+Time all: solve [solve_P].
 Qed.
 
 Lemma test_ok x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T2: parallel".
-Time par: solve_P.
+Time par: solve [solve_P].
 Qed.
 
 Lemma test_fail x : P (S x) /\ P x /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T3: linear failure".
-Fail Time all: solve_P.
-all: apply (P_triv Type).
+Fail Time all: solve solve_P.
+all: solve [apply (P_triv Type)].
 Qed.
 
 Lemma test_fail2 x : P (S x) /\ P x /\ P (S x) /\ P (S x).
 Proof.
 repeat split.
 idtac "T4: parallel failure".
-Fail Time par: solve_P.
-all: apply (P_triv Type).
+Fail Time par: solve [solve_P].
+all: solve [apply (P_triv Type)].
 Qed.