Repeatedly processing the same text gives errors with quote-nested Elpi metavariables

[patrick-nicodemus]

I think this is a bug but I am not sure. I am new to Elpi.

How to replicate:

1. Open this in a fresh file in VSCode. https://github.com/LPCIC/coq-elpi/blob/master/examples/example_record_to_sigma.v
2. Process the text, put cursor at the end and hit Alt-R
3. Move the cursor to of the head of document, before "From elpi Require Import elpi" and hit Alt-R
4. Move the cursor to the end of the document and hit Alt-R
   This yields an error saying that in the clause

wrap-fields-bo.aux [X|XS] {{ sigT lp:F }} {{ existT lp:F lp:X lp:Rest }} :-
  F = fun _ _ G,
  wrap-fields-bo.aux XS (G X) Rest.

"The reference F is not found in the global environment."

The problem seems to occur more generally with Elpi variables nested within Coq quotes, as in this example.
It seems to be necessary that the user runs the "From elpi Require Import elpi" command twice to cause the bug?
One gets around the problem by using the Coq reset command, Alt-Home.

[gares]

Yes, you cannot unload Elpi. This is not really specific to Elpi, but to plugins extending Coq grammar.