Maxime Dénès (Mar 06 2022 at 17:09): Maxime Dénès (Mar 06 2022 at 17:09):I'm wondering why Tactic Notation uses kernel names for grammar extensions : https://github.com/coq/coq/blob/master/plugins/ltac/tacentries.ml#L272
Maxime Dénès (Mar 06 2022 at 17:11):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.
Maxime Dénès (Mar 06 2022 at 17:11):I guess @Pierre-Marie Pédrot may know more :)
Pierre-Marie Pédrot (Mar 06 2022 at 22:19):What would you use instead? Despite the name, tactic notations are not notations, they really extend the Ltac runtime.
Pierre-Marie Pédrot (Mar 06 2022 at 22:24):(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.)
Maxime Dénès (Mar 06 2022 at 23:22):I mean: why are they used for grammar extensions, and not just for the interpretation part of Tactic Notation?
Maxime Dénès (Mar 06 2022 at 23:24):My question is not philosophical :) I simply have a hard time following the code in pcoq and lower parsing layers
Maxime Dénès (Mar 06 2022 at 23:25):So I don't know what the kernel name passed to extend_tactic_grammar is used for.
Maxime Dénès (Mar 06 2022 at 23:34):Ah but ok, I understand now, it comes back to add_tactic_entry.
Last updated: Jun 09 2023 at 07:01 UTC