Skip to content
Snippets Groups Projects

More missing `Hint Mode`s.

Merged 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

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
Please register or sign in to reply
Loading