coq.env.add-indt fails to add universe polymorphic inductives when not in a section

[ecranceMERCE]

Declaring a new universe polymorphic inductive type with coq.env.add-indt fails when not in a section.

From elpi Require Import elpi.
Set Universe Polymorphism.

Elpi Tactic test.

(* Section Test. *)

Elpi Query lp:{{
  coq.univ.new U,
  coq.univ.variable U L,
  @udecl! [L] tt [] tt =>
    coq.env.add-indt (inductive "MyFalse" tt (arity (sort (typ U))) (i\ [])) I.
}}.

No open section.

Uncommenting the line before the Elpi query makes the error vanish.

[ecranceMERCE]

Issue https://github.com/LPCIC/coq-elpi/issues/374 might be related as the error message is the same.

[ecranceMERCE]

I think this bug came from the fact I tried to edit poly in this line, so maybe I opened an issue that does not concern master, and if that's the case I am sorry.

Nevertheless, I still do not understand why everything works even when leaving this boolean to false. It's counter-intuitive to declare polymorphic inductives by saying the universe context is not polymorphic...

But in the Coq API, it calls some section function in the poly case, which causes the bug if the boolean is true.