Deprecate unqualified "Instance"
With !594 (merged) (and potentially some follow-up changes), all Hint
in Iris will be qualified with Local
or Global
. I think we should do the same with Instance
.
@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?