I'm wondering why Tactic Notation
uses kernel names for grammar extensions : https://github.com/coq/coq/blob/master/plugins/ltac/tacentries.ml#L272
It makes separation of parsing and execution a bit tricky because this kernel name is generated by a gensym, so I'd like to understand why its use is not limited to interpretation.
I guess @Pierre-Marie Pédrot may know more :)
What would you use instead? Despite the name, tactic notations are not notations, they really extend the Ltac runtime.
(You can probably get rid of the gensym but then you have to be careful to get a reproducible name with a low probability of conflict out of the production list.)
I mean: why are they used for grammar extensions, and not just for the interpretation part of Tactic Notation
?
My question is not philosophical :) I simply have a hard time following the code in pcoq
and lower parsing layers
So I don't know what the kernel name passed to extend_tactic_grammar
is used for.
Ah but ok, I understand now, it comes back to add_tactic_entry
.
Last updated: Jun 09 2023 at 07:01 UTC