Use hint mode + more often (!435) · Merge requests · Iris / stdpp · GitLab

Robbert Krebbers requested to merge ralf/hint-mode-plus into master Dec 15, 2022

This is the result of the discussion at https://mattermost.mpi-sws.org/iris/pl/wpjk3kpbx7bf5brh7o3319c8uo