Adapt w.r.t. coq/coq#12512. (!464) · Merge requests · Iris / Iris · GitLab

The source project of this merge request has been removed.

Ghost User requested to merge (removed):globref-in-auto-using into master Jun 16, 2020

See stdpp!165 (closed).