The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Here is a workaround that I use.

Goal False.

assert (forall (A B C:Type), A->B->C) as H by admit.

specialize (fun A a C => H A nat C a O).

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Dec 23, 2015 at 10:36 AM, Pierre Courtieu <Pierre.Courtieu AT cnam.fr> wrote:

Hi,

[specialize] is kind of useful but it needs a list of concrete terms
for a *prefix* of list of premisses of a hypothesis.

AFAIK you cannot give only, say, 3rd and 5th arguments. Sometime this
would be useful (because the hypothesis has independent premisses and
no particular order in the hyps is better than another).

Is there something to do so? I have a Ltac piece of code which does
roughly this in a naive way, but it is limited to one argument at a
time.

Idealy I would like to write:

generalize H with (x:=0) (3:=H2)(5:=H6).

Is this creatively hackable in ltac :) ?

Best regards,
Pierre