Adapt w.r.t. coq/coq#18909.#1881

Merged

andres-erbsen merged 1 commit intomit-plv:masterfrom ppedrot:hint-using-strict-globref

Apr 18, 2024

Commits on Apr 18, 2024

Adapt w.r.t. rocq-prover/rocq#18909 .
ppedrot
committed