Locating inside module can lead to anomaly

[trilis]

[Copied from discussion of #618 as separate issue]

On this code

From elpi Require Import elpi.
Require Import String.

Class Show (A : Type) :=
  { show : A -> string }.

Elpi Command ElpiTest.
#[synterp] Elpi Accumulate lp:{{
    main _ :-
        coq.env.end-module _.
}}.
Elpi Accumulate lp:{{
    main _ :-
        coq.env.add-const "x"
            {{ Build_Show string (@id string) }} 
            {{ Show string }} @transparent! _,
        coq.locate "x" G,
        coq.TC.declare-instance G 0,
        coq.env.end-module _.
}}.
Elpi Typecheck.
Elpi Export ElpiTest.

Module A. 
ElpiTest.

We get

Error: Anomaly "Constant Test.x does not appear in the environment."
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Environ.lookup_constant in file "kernel/environ.ml" (inlined), line 217, characters 6-34
Called from Typeops.type_of_global_in_context in file "kernel/typeops.ml", line 598, characters 13-42
Called from Classes.existing_instance in file "vernac/classes.ml", line 300, characters 20-59
...

So it looks like the anomaly is thrown when declaring instance. Maybe there is some case of FQN confusion? Because it probably shouldn't be Test.x, it should be Test.A.x (Test is the name of my file). But changing locate string to "A.x" results in locate failure. Note that synterp code closing the module is essential to reproduce this — can it be that closing module in synterp somehow messes with interp code?

(Of course, one can easily circumvent this issue by using output of add-const instead of locating, but I think it's an interesting finding nevertheless)

[trilis]

I can confirm that #620 fixes this also. Thank you @Janno!