Deprecate unqualified "Instance"
With !594 (merged) (and potentially some follow-up changes), all
Hint in Iris will be qualified with
Global. I think we should do the same with
@tchajed is there a way to adjust your script to do that, or will we have to ask the Coq devs for an (opt-in) deprecation warning for
Instance first, similar to the
Hint warning that your script is based on?