The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Using uconstr probably works, something like

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

Tactic Notation "program_data_destruct" uconstr(st) ident(ll) ident(glob) 
ident(H) :=
  (program_data_destruct_impl st ll glob H).

Gaëtan Gilbert

On 19/07/2023 17:30, Chris Dams wrote:
> 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