Say I have one module declared as follows in file A.v:

Section A.
  Context {𝒳 : Set}.
  Inductive abt := Abt_leaf (x : 𝒳) | Abt_node.
End A.

Now in another file B.v, I have

Require Import A.
Definition 𝒳 := nat.
Inductive typ := Tpe_num | Typ_str.
Definition typ_to_abt (t : typ) : abt (* @abt 𝒳 *) := Abt_node.

The implicit arguments in abt when defining typ_of_abt can't be inferred. How to let Coq know I always want abt to be @abt 𝒳 in B.v? The intent is to avoid explicitly specifying them using @.

Thanks.