Merged requested to merge robbert/hintmode into master
This MR adds all the
Hint Modes from @Blaisorblade's iris!696 (merged) to std++ with the exception of the controversial one for
Equiv (see https://github.com/coq/coq/issues/14441), but including the ones for
Iris requires a one line fix, see iris!696 (comment 68611)
examples, reloc, iron, actris, and lambdarust all compile without changes.
I think we're still missing more
Hint Modes, but I am not sure what's a proper way to detect them.