The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 15/01/2014 17:16, Jason Gross wrote:
> I would like to revive this thread, now that new-tacticals and
> Paral-ITP have landed in trunk.  In particular, I'd like to know if
> any of the new tacticals implement this parallel behavior, and if I
> can expect/ask for there to be a parallel equivalent of "; abstract
> tac" for 8.5. (Apologies if I missed some email explaining that there
> is such a tactic.)

Well, the Paral-ITP has somehow simplified the trickiness of the cases
presented here by providing a generic way to manipulate side-effects,
but the state mechanism is not fine-grained enough to handle this level
of detail.

So in essence, I won't be able to use the slave mechanism to do it, but
yes, I can still rely on forking the process as in my previous plugin...
If you're OK with the price to pay to fork, it should be doable.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature