The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

Hello,

I was essentially trying to write some tactic combinator that would accept a one-argument tactic as input, and call this tactic with some hypothesis. My problem is that I have managed to make it work with pre-defined tactics, but not with on-the-fly anonymous tactics. See:

Ltac idtac' := idtac.

Ltac idtac'' x := idtac x.

Ltac silly tactic arg := tactic arg.

Goal forall (T : Type), False.

  intros.

  (* 0: Illegal tactic application *)

  Fail silly idtac T.

  (* 1: Illegal tactic application *)

  Fail silly idtac' T.

  (* 2: OK *)

  silly idtac'' T.

  (* 3: The reference idtac was not found in the current environment. *)

  Fail silly (fun x => idtac x) T.

  (* 4: x not found *)

  Fail silly (fun x => ltac:(idtac x)) T.

  (* 5: The reference idtac' was not found in the current environment. *)

  Fail silly (fun x => idtac' x) T.

  (* 6: Illegal tactic application *)

  Fail silly (fun x => ltac:(idtac' x)) T.

  (* 7: The reference idtac'' was not found in the current environment. *)

  Fail silly (fun x => idtac'' x) T.

  (* 8: Cannot infer the type of x in environment:

     T : Type *)

  Fail silly (fun x => ltac:(idtac'' x)) T.

  (* 9: Cannot infer an internal placeholder of type "Type" in environment:

     T : Type

     x : Type *)

  Fail silly (fun (x : Type) => ltac:(idtac'' x)) T.

I think by the end of this (attempts 8 and 9), I'm actually confused as to what I am manipulating, and what the internal placeholder is.

Is there a way to make such a combinator so that I can call:

silly (fun x => ltac:(someTactic x)).

Or is there some fundamental issue with manipulating anonymous tactics?

Best regards,

- Valentin