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
H is a
qualid and also a local variable contradicted to the
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”?