handle tactic argument properly

[ggrov]

Normal (non-env) tactics that are arguments are currently ignored by the K combinator. This has to be fixed.

[lyhlbyl]

a proper fix to this issue is to add a filed in the atomic tactic indicating the number of arguement in the tactic. For now, we can use a provide a dummy definition, e.g.
tactic T := T;
to skip the "K"

[ggrov]

I agree. The dummy solution will have to work for now, but does not look particularly nice...

[ggrov]

By the way, how about give env tactics a type env? E.g. mytac : env instead of ENV_mytac?