Trocq interaction with sections

[MysaaJava]

Trocq database interacts wrongly with sections variables.
Here is a failing example (on my personal branch with Print Translations):

From Trocq Require Import Trocq.

Set Universe Polymorphism.

Section sum.

    Variable (A A' : Type) (AR : Param01.Rel A A') (B B': Type)
        (BR: Param01.Rel B B').

    Definition inlA : A -> sum A B := fun a => inl a.

    Definition inlA' : A' -> sum A' B' := fun a' => inl a'.

    Definition inlR' a a' (aR: AR a a') :
      Param01_sum A A' AR B B' BR (inlA a) (inlA' a') := inlR A A' AR B B' BR a a' aR.
    
    Structure eqType := EqType { sort : Type; equal : sort -> sort -> bool }.

    Trocq Use inlR'.
    
    (* We have registered inlR' in translations *)
    Trocq Print Translations.

End sum.

(* inlR' is still registered here, even though it depended on section variables *)
Trocq Print Translations.

Goal forall A (a: A), inlA A A a = inlA A A a.
    trocq. (* Fails *)
Abort.