Open
Description
For example, with the coq-elpi plugin, we can write the following Vernacular command. But PG doesn't recognize the proper end of the command when we do C-c C-n.
https://github.com/LPCIC/coq-elpi/blob/6d21fa61fb59a555c5075ba3e3c89844a5d14bee/theories/tutorial/elpi_lang.v#L53-L58
Elpi Program tutorial lp:{{
kind person type.
type mallory, bob, alice person.
}}.
This quotation mechanism lp:{{ ... }} is introduced by rocq-prover/rocq#9733. Since the delimiters can be nested, I think that we need a recursive grammar (CFG, PEG, etc.) to detect the end of commands, and couldn't write regexps like coq-end-command-regexp(-backward) anymore to detect it. But I wonder that PG handled the following command properly.
idtac (* (* *) . *).Does anyone have a workaround or fix for this problem?
cc: @gares
Metadata
Metadata
Assignees
Labels
No labels