Imported Upstream version 8.5~beta1+dfsg

1 files changed, 46 insertions, 0 deletions

diff --git a/test-suite/success/paralleltac.v b/test-suite/success/paralleltac.v
new file mode 100644
index 00000000..94ff96ef
--- /dev/null
+++ b/test-suite/success/paralleltac.v
@@ -0,0 +1,46 @@
+Fixpoint fib n := match n with
+  | O => 1
+  | S m => match m with
+    | O => 1
+    | S o => fib o + fib m end end.
+Ltac sleep n :=
+  try (assert (fib n = S (fib n)) by reflexivity).
+(* Tune that depending on your PC *)
+Let time := 18.
+
+Axiom P : nat -> Prop.
+Axiom P_triv : Type -> forall x, P x.
+Ltac solve_P :=
+  match goal with |- P (S ?X) =>
+    sleep time; exact (P_triv Type _)
+  end.
+
+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.
+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.
+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).
+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).
+Qed.