GitLab

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?