Confused with qualid

Developing the Rocq Prover
1

By definition of Coq documentation,
Identifiers may also denote local variables, while qualified identifiers do not.
It is no problem to say that “qualid denotes global objects”.

However, I found in the tactic apply H, H is a qualid and also a local variable contradicted to the
documentation.

So my question is whether it is precise enough to say “qualid denotes global objects”.
To be more precise, shall I adopt “qualid usually denotes global objects”?

2

The issue with this formulation “qualified identifiers do not” is that it neglects the fact that simple identifiers are also qualified identifiers (with an empty path qualifying the identifier). As you noticed, apply takes a qualid which may denote a global or a local object. But as soon as the qualid is of the form foo.bar, then it cannot be a local object.

Feel free to contribute to improving the documentation when you notice such glitches!