The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Hi

I'm trying to do

Ltac apply2 th1 th2 := apply th1 || apply th2.

Ltac sqr_simpf applyf  :=
list_assoc_r ; repeat (applyf sqr_appL1 || applyf sqr_appL2 ||
... (ie lots more of the same)

Ltac sqr_simps th1 := sqr_simpf (ltac:(apply2) th1).

sqr_simps
But then trying to use sqr_simps I get

sqr_simps sqr_sctr_relRI.
 > ^^^^^^^^^
Error:
In nested Ltac calls to "sqr_simps" and "(_ th1)" (with 
th1:=sqr_sctr_relRI),
last term evaluation failed.
The user-defined tactic "k4_inv.apply2" was not fully applied:
There are missing arguments for variables th1 and th2,
no arguments at all were provided.

But the first argument is given as sqr_sctr_relRI (ie it gets plugged in 
for th1), and the second argument is given at each call of applyf in the
body of sqr_simpf

this gives a similar message

 > sqr_simpf (ltac:(apply2) sqr_sctr_relRI).
 >            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
The user-defined tactic "k4_inv.apply2" was not fully applied:
There are missing arguments for variables th1 and th2,
no arguments at all were provided.

this gives a slightly different message

 > sqr_simpf (ltac:(apply2 sqr_sctr_relRI)).
 >            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error:
The user-defined tactic "k4_inv.apply2" was not fully applied:
There is a missing argument for variable th2,
an argument was provided for variable th1.

Also I tried this: (which isn't actually what I want to do)

sqr_simpf (ltac:(apply)).
 >            ^^^^^^^^^^^^
Error:
In nested Ltac calls to "_" and "apply", last call failed.
No product even after head-reduction.

thanks,

Jeremy