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.
Hint Mode
Equiv
Set
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.
00:04:52
3 years ago
No artifacts found
00:04:50
00:04:45
