Hi,
I'm having difficulty using the tactic
Variant instantiate (num := term)
because I get
lja_dd_ImpL_p < instantiate (0 := l).
Toplevel input, characters 1-21:
> instantiate (0 := l).
> ^^^^^^^^^^^^^^^^^^^^
Error:
Ltac call to "instantiate ( (int) := (lglob) ) (hloc)" failed.
Incorrect existential variable index.
lja_dd_ImpL_p < instantiate (1 := l).
Toplevel input, characters 0-20:
> instantiate (1 := l).
> ^^^^^^^^^^^^^^^^^^^^
Error:
Ltac call to "instantiate ( (int) := (lglob) ) (hloc)" failed.
Not enough uninstantiated existential variables.
Are existential variables numbered from 0 or from 1?
And what am I doing wrong?
Thanks
Jeremy