It seems that `lp:{{`

blocks can be terminated in the same line as a `%`

comment, and braces `{{`

can be nested in such comments:

```
From elpi Require Import elpi.
Elpi Program w lp:{{
% {{
% }} }}.
```

How is the end of an antiquotation determined exactly? I'm adding elpi support to coqtail and I'm not sure how to understand this corner case. I'm currently just ignoring the rest of the line after a `%`

but that's not what the Coq/elpi parser is doing.

You have to think that in order to find the end, you don't need the elpi parser. Coq has to parse the string without calling elpi, so % is no different than, say, x. just count for {{ and }}.

Then I believe it is a bit smarter than that, as in you can start with any number of { and the end is when you find the same. But for example vscoq does not understand that.

https://github.com/coq/coq/blob/f2bf445b8f4f5241ebdc348b69961041b4e57883/parsing/cLexer.ml#L542

Last updated: Jun 06 2023 at 23:01 UTC