The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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.)

-Jason

On Fri, Jun 21, 2013 at 10:32 AM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 21/06/2013 16:07, Enrico Tassi wrote:
> I did not look at the code, but I'm curious.  What happens if you do:
>
>   assert True >> [ abstract( exact I ) | idtac ].
>
> And in the even more trickier case, if you do:
>
>   Goal (Type /\ Type) /\ True.
>   split; [ split >> [ exact Type | exact Type ] | exact Type ].
>
> which is the resulting proof term?
>  (Conj (Conj Type_i Type_i) Type_i)  or  (Conj (Conj Type_i Type_j) Type_k)

In the first case, it will die in a horrible suffering, because of the
current implementation of abstract (and admit) whose defects you're
aware of.

I admit that I did not think about the second case, which is tricky
indeed. Nonetheless, it is quite easy to freshen the universes in the
generated term, and let the universe constraint solver deal with it.

PMP