In "A Unification Algorithm for COQ Featuring Universe Polymorphism and Overloading", Ziliani and Sozeau say:
Terms include variables $x \in \mathcal{V}$, constants $c \in > \mathcal{C}$, inductive type constructors $i \in \mathcal{I}$ and constructors $k \in \mathcal{K}$, these last three being applied to universe instances $\bar{\ell}$ built from universe levels $\ell \in \mathcal{L}\cup 0^-$.
Now, $\mathcal{L}$ I recognize as Gödel's constructible universe, but what's $0^{-}$? And while I'm at it, what does it mean to "apply" a constant to a universe instance - as in $c|\bar\ell|$?
$\newcommand{\L}{\mathcal{L}}$It’s just a formal symbol. That is, by $\L \cup 0^-$ they mean the set $\L$ with one extra new element added, and they take $0^-$ as the name for that extra element.
While we’re at it, $\L$ is certainly not Gödel’s constructible universe here. I don’t think they explicitly say so in this paper, but if I understand right, $\L$ is just assumed to be some set of formal symbols used to represent universe levels — just like the set of “variables” that most treatments of syntax assume as a given, but they need a second such set here, to keep universe levels distinct from ordinary variables in their syntax. So it can be any infinite set.
(If you’re thinking of this as happening in a constructive meta-theory — which I am, and I guess Sozeau/Ziliani may well have been — then you will probably need to add the assumption that $\L$ has decidable equality. Again, I’m just copying the standard assumptions made for sets of variables used in syntax.)