Stream: Coq users

Topic: KerName in tactic


view this post on Zulip liao zhang (Jun 16 2020 at 14:53):

I am confused with what role does KerName plays in tactic sentence.
“auto” is referred by KerName.
Does it mean all the KerName in tactic sentence point to some internal tactics like “auto”?
Is there any argument point by KerName? For example “apply X”, which X is pointed by KerName?

view this post on Zulip Pierre-Marie Pédrot (Jun 16 2020 at 16:33):

only global tactics, like the one you define via Ltac foo := ... have a kernel name

view this post on Zulip liao zhang (Jun 16 2020 at 20:55):

Pierre-Marie Pédrot said:

only global tactics, like the one you define via Ltac foo := ... have a kernel name

Thanks very much!


Last updated: Feb 06 2023 at 13:03 UTC