Remove obsolete `Hint Extern`s that predate the `Hint Mode` declarations.
Passed
Robbert Krebbers
created pipeline for commit
9a1b4cde
, finished
For master
9 minutes 41 seconds, queued for 2 seconds