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
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
Last updated: Dec 05 2023 at 05:01 UTC