LPCIC / coq-elpi

Coq plugin embedding elpi
GNU Lesser General Public License v2.1
139 stars 51 forks source link

Redoing `Require Import elpi` breaks the parser #214

Closed pi8027 closed 2 years ago

pi8027 commented 3 years ago

The following code fails

From elpi Require Import elpi.
Back.
From elpi Require Import elpi.

Elpi Db test.db lp:{{
test {{ lp:T }}.
}}.

with the following message:

$ coqtop < test.v
Welcome to Coq 8.13.0 (January 2021)

Coq < [Loading ML file ring_plugin.cmxs ... done]
[Loading ML file zify_plugin.cmxs ... done]
[Loading ML file micromega_plugin.cmxs ... done]
[Loading ML file omega_plugin.cmxs ... done]
[Loading ML file int63_syntax_plugin.cmxs ... done]
[Loading ML file float_syntax_plugin.cmxs ... done]
[Loading ML file elpi_plugin.cmxs ... done]

Coq <
Coq <
Coq < Coq < Coq < Coq < Toplevel input, characters 4-5:
Error: The reference T was not found in the current environment.

It works fine if I remove Back.

gares commented 3 years ago

I know, and I'm afraid it is unfixable without LPCIC/elpi#13 see also #112.