In large, complex proofs it is sometimes difficult to make the overall argument parallel (due to linear `Require`

dependencies). However, it is common practice in individual proofs to see e.g.

```
apply lemma1; [ auto | firstorder | ].
apply lemma2; [ trivial | auto | ].
rest_of_proof...
```

In particular, applying `lemma1`

and `lemma2`

creates several (here three) subgoals, of which only one (here the third) is particularly interesting and the others can be solved by automation individually (also contain no evars).

More often than not, heavy automation increases compilation time.

Assume in the above `auto`

, `firstorder`

, and `rest_of_proof`

take roughly the same time to compile.

**Suggestion** (is the following interesting/feasible?):

Introduce a tactical `async`

such that given a tactic `t`

, the tactic `async t`

succeeds immediately (if the goal has no evars) and closes the goal. Simultaneously, a worker is spawned that is responsible to actually close the goal using the tactic `t`

until `Qed`

.

Returning to the above example

```
apply lemma1; [ async auto | async firstorder | ].
apply lemma2; [ trivial | async auto | ].
rest_of_proof...
```

would (given at least 4 CPU cores) compile several times faster. I know of `par:`

, which does not seem to fit the above use case.

Before adding another [wish] to the Coq bugtracker, I wanted to know your opinion. Somewhat related: #9550