Record fields are not visible from outside the module if the record is universe polymorphic

[ecranceMERCE]

I try to declare the following record with Coq-Elpi in a module Test:

Record Rec : Type := BuildRec { f : Type }.

From elpi Require Import elpi.
Set Universe Polymorphism.

Elpi Command x.
Elpi Query lp:{{
  coq.env.begin-module "Test" none,
  Decl = record "Rec" {{ Type }} "BuildRec" (field [] "f" {{ Type }} (_\ end-record)),
  % @univpoly! =>
    coq.env.add-indt Decl _,
  coq.env.end-module _.
}}.

Print Module Test.
Check Test.f.

The Print command gives this:

Module Test := Struct
  Record Rec : Type := BuildRec { f : Type }.
  Definition f : forall _ : Rec, Type.
End

and the Check succeeds.

Now uncomment the option to make the record polymorphic and boom:

Module Test := Struct Record Rec@{u u0} : Type := BuildRec { f : Type }. End

The field f is not exported and the Check now fails.

cc @CohenCyril

[ecranceMERCE]

The bug is even present without opening a module. Actually, it is just that a polymorphic record declaration through Coq-Elpi does not export the fields.

Elpi Query lp:{{
  @univpoly! =>
    coq.env.add-indt (record "R" {{ Type }} "BuildR" (field [] "a" {{ Type }} (a\ end-record))) _.
}}.
Fail Check a.

(commenting the option makes the Check valid)

[gares]

I guess the field (the projection) is not generated for some bug. The projection is a regular constant synthesized by coq, I guess it does not typecheck because of the bug....