Skip to content

More missing `Hint Mode`s.

Robbert Krebbers 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 Sets.

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.

Merge request reports