Remove the few instances of non-global hint declarations.#126

Merged

spitters merged 1 commit intocoq-community:masterfrom ppedrot:rm-hint-constr

Apr 7, 2024

+11-4

Commits on Apr 7, 2024

Remove the few instances of non-global hint declarations.
ppedrot
committed