The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear All,

I would like to be able to use a pattern as an argument to an Ltac
tactic. Is this somehow possible? At the moment I am running into:

Ltac program_data_destruct st ll glob H
:= destruct st as [ll glob|] eqn:H;
     [fold mk_program_data in H |- * | fold mk_program_data_error in H |- *].

I would like to use a pattern instead of a complete term for st
because what I would like to pass as st can be quite large and I like
to fill in a few parameters to indicate which instance I want to
destruct but not all of them because that would be a bit too large.
E.g., I would like to do

program_data_destruct (set_pointer (mk_program_data _ _) _ _ _) ll' glob' H4.

but that runs into the error 'Cannot infer this placeholder of type
"program.stack program_global_type_info"'. Note that it would be quite
possible to pass the pattern term (set_pointer (mk_program_data _ _) _
_ _) as an argument to the destruct tactic, it is just the Ltac macro
that apparently forbids using this pattern term.

Is it possible to make this work somehow?

Kind Regards,
Chris